| 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) |
A (constructor)
Abort [in MetaRocq.Examples.tauto]abs_red_r [in MetaRocq.Template.Typing]
abs_red_l [in MetaRocq.Template.Typing]
abs_red_r [in MetaRocq.PCUIC.PCUICReduction]
abs_red_l [in MetaRocq.PCUIC.PCUICReduction]
ahyp [in MetaRocq.Erasure.EInduction]
all [in MetaRocq.Template.TemplateMonad.Common]
AllEqual [in MetaRocq.Common.Universes]
AllIrrelevant [in MetaRocq.Common.Universes]
Alli_cons [in MetaRocq.Utils.All_Forall]
Alli_nil [in MetaRocq.Utils.All_Forall]
all_nth_error_None [in MetaRocq.Erasure.Typed.Annotations]
all_nth_error_Some [in MetaRocq.Erasure.Typed.Annotations]
all_submodules_except [in MetaRocq.Quotation.ToPCUIC.Init]
all_submodules_except [in MetaRocq.Quotation.ToTemplate.Init]
All_fold_cons [in MetaRocq.Utils.All_Forall]
All_fold_nil [in MetaRocq.Utils.All_Forall]
All_cons [in MetaRocq.Utils.All_Forall]
All_nil [in MetaRocq.Utils.All_Forall]
All2i_len_cons [in MetaRocq.Utils.All_Forall]
All2i_len_nil [in MetaRocq.Utils.All_Forall]
All2i_cons [in MetaRocq.Utils.All_Forall]
All2i_nil [in MetaRocq.Utils.All_Forall]
All2_eval_app_intro [in MetaRocq.Erasure.Typed.WcbvEvalAux]
All2_fold_cons [in MetaRocq.Utils.All_Forall]
All2_fold_nil [in MetaRocq.Utils.All_Forall]
All2_dep_cons [in MetaRocq.Utils.All_Forall]
All2_dep_nil [in MetaRocq.Utils.All_Forall]
All2_cons [in MetaRocq.Utils.All_Forall]
All2_nil [in MetaRocq.Utils.All_Forall]
All2_cons [in MetaRocq.Erasure.EPrimitive]
All2_nil [in MetaRocq.Erasure.EPrimitive]
All3_cons [in MetaRocq.Utils.All_Forall]
All3_nil [in MetaRocq.Utils.All_Forall]
AlreadyDeclared [in MetaRocq.SafeChecker.PCUICErrors]
AlreadyDeclared [in MetaRocq.Template.Checker]
And [in MetaRocq.Examples.tauto]
app [in MetaRocq.Examples.add_constructor]
App_r [in MetaRocq.PCUIC.Syntax.PCUICPosition]
App_l [in MetaRocq.PCUIC.Syntax.PCUICPosition]
app_r [in MetaRocq.PCUIC.Syntax.PCUICPosition]
app_l [in MetaRocq.PCUIC.Syntax.PCUICPosition]
app_red_r [in MetaRocq.Template.Typing]
app_red_l [in MetaRocq.Template.Typing]
app_red_r [in MetaRocq.PCUIC.PCUICReduction]
app_red_l [in MetaRocq.PCUIC.PCUICReduction]
Args [in MetaRocq.SafeChecker.PCUICSafeConversion]
arity_spine_ass [in MetaRocq.PCUIC.PCUICSpine]
arity_spine_def [in MetaRocq.PCUIC.PCUICSpine]
arity_spine_conv [in MetaRocq.PCUIC.PCUICSpine]
arity_spine_nil [in MetaRocq.PCUIC.PCUICSpine]
ArrayNotConvertibleDefault [in MetaRocq.SafeChecker.PCUICErrors]
ArrayNotConvertibleLevels [in MetaRocq.SafeChecker.PCUICErrors]
ArrayNotConvertibleTypes [in MetaRocq.SafeChecker.PCUICErrors]
ArrayNotConvertibleValues [in MetaRocq.SafeChecker.PCUICErrors]
ArrayValuesNotSameLength [in MetaRocq.SafeChecker.PCUICErrors]
array_val [in MetaRocq.PCUIC.Syntax.PCUICPosition]
array_ty [in MetaRocq.PCUIC.Syntax.PCUICPosition]
array_def [in MetaRocq.PCUIC.Syntax.PCUICPosition]
array_red_type [in MetaRocq.Template.Typing]
array_red_def [in MetaRocq.Template.Typing]
array_red_val [in MetaRocq.Template.Typing]
array_red_type [in MetaRocq.PCUIC.PCUICReduction]
array_red_def [in MetaRocq.PCUIC.PCUICReduction]
array_red_val [in MetaRocq.PCUIC.PCUICReduction]
assumption_context_vass [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
assumption_context_nil [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
atomic_array [in MetaRocq.Template.WcbvEval]
atomic_atom [in MetaRocq.Template.WcbvEval]
atomic_primitive [in MetaRocq.Erasure.EWcbvEval]
atomic_atom [in MetaRocq.Erasure.EWcbvEval]
atomic_primitive [in MetaRocq.PCUIC.PCUICWcbvEval]
atomic_atom [in MetaRocq.PCUIC.PCUICWcbvEval]
| 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) |