| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (19204 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (228 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (298 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1273 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (313 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (8163 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1514 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (52 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (352 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (534 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (727 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (402 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (333 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4833 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (182 entries) |
O (constructor)
O [in MetaRocq.Examples.demo]Ok [in MetaRocq.Erasure.Typed.ResultMonad]
only_toplevel [in MetaRocq.Quotation.ToPCUIC.Init]
only_toplevel [in MetaRocq.Quotation.ToTemplate.Init]
OnOne2All_tl [in MetaRocq.Utils.All_Forall]
OnOne2All_hd [in MetaRocq.Utils.All_Forall]
OnOne2i_tl [in MetaRocq.Utils.All_Forall]
OnOne2i_hd [in MetaRocq.Utils.All_Forall]
onone2_localenv_cons_tl [in MetaRocq.PCUIC.utils.PCUICOnOne]
onone2_localenv_def [in MetaRocq.PCUIC.utils.PCUICOnOne]
onone2_localenv_cons_abs [in MetaRocq.PCUIC.utils.PCUICOnOne]
OnOne2_tl [in MetaRocq.Utils.All_Forall]
OnOne2_hd [in MetaRocq.Utils.All_Forall]
onPrimArray [in MetaRocq.PCUIC.utils.PCUICPrimitive]
onPrimFloat [in MetaRocq.PCUIC.utils.PCUICPrimitive]
onPrimInt [in MetaRocq.PCUIC.utils.PCUICPrimitive]
onPrimsArray [in MetaRocq.Erasure.EPrimitive]
onPrimsArray [in MetaRocq.PCUIC.utils.PCUICPrimitive]
onPrimsArrayDep [in MetaRocq.Erasure.EPrimitive]
onPrimsArray_dep [in MetaRocq.PCUIC.utils.PCUICPrimitive]
onPrimsFloat [in MetaRocq.Erasure.EPrimitive]
onPrimsFloat [in MetaRocq.PCUIC.utils.PCUICPrimitive]
onPrimsFloatDep [in MetaRocq.Erasure.EPrimitive]
onPrimsFloat_dep [in MetaRocq.PCUIC.utils.PCUICPrimitive]
onPrimsInt [in MetaRocq.Erasure.EPrimitive]
onPrimsInt [in MetaRocq.PCUIC.utils.PCUICPrimitive]
onPrimsIntDep [in MetaRocq.Erasure.EPrimitive]
onPrimsInt_dep [in MetaRocq.PCUIC.utils.PCUICPrimitive]
onPrimsString [in MetaRocq.Erasure.EPrimitive]
onPrimsString [in MetaRocq.PCUIC.utils.PCUICPrimitive]
onPrimsStringDep [in MetaRocq.Erasure.EPrimitive]
onPrimsString_dep [in MetaRocq.PCUIC.utils.PCUICPrimitive]
onPrimString [in MetaRocq.PCUIC.utils.PCUICPrimitive]
on_force [in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd]
on_lazy [in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd]
on_prim [in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd]
on_cofix [in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd]
on_fix [in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd]
on_proj [in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd]
on_case [in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd]
on_cstr [in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd]
on_app [in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd]
on_letin [in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd]
on_lambda [in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd]
on_evar [in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd]
on_atom [in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd]
on_force [in MetaRocq.Erasure.EWcbvEvalEtaInd]
on_lazy [in MetaRocq.Erasure.EWcbvEvalEtaInd]
on_prim [in MetaRocq.Erasure.EWcbvEvalEtaInd]
on_cofix [in MetaRocq.Erasure.EWcbvEvalEtaInd]
on_fix [in MetaRocq.Erasure.EWcbvEvalEtaInd]
on_proj [in MetaRocq.Erasure.EWcbvEvalEtaInd]
on_case [in MetaRocq.Erasure.EWcbvEvalEtaInd]
on_app [in MetaRocq.Erasure.EWcbvEvalEtaInd]
on_letin [in MetaRocq.Erasure.EWcbvEvalEtaInd]
on_lambda [in MetaRocq.Erasure.EWcbvEvalEtaInd]
on_evar [in MetaRocq.Erasure.EWcbvEvalEtaInd]
on_atom [in MetaRocq.Erasure.EWcbvEvalEtaInd]
on_force [in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksInd]
on_lazy [in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksInd]
on_prim [in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksInd]
on_cofix [in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksInd]
on_fix [in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksInd]
on_proj [in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksInd]
on_case [in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksInd]
on_cstr [in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksInd]
on_app [in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksInd]
on_letin [in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksInd]
on_lambda [in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksInd]
on_evar [in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksInd]
on_atom [in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksInd]
option_ext_non [in MetaRocq.Utils.MROption]
option_ext_keep [in MetaRocq.Utils.MROption]
option_ext_fill [in MetaRocq.Utils.MROption]
Or [in MetaRocq.Examples.tauto]
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (19204 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (228 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (298 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1273 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (313 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (8163 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1514 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (52 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (352 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (534 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (727 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (402 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (333 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4833 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (182 entries) |