| 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) |
E (abbreviation)
EnvironmentReflect.extendsb_decls_part [in MetaRocq.Common.EnvironmentReflect]EnvironmentReflect.strictly_extendsb_decls_part [in MetaRocq.Common.EnvironmentReflect]
Environment.context_decl [in MetaRocq.Common.Environment]
Environment.extends_decls_part [in MetaRocq.Common.Environment]
Environment.extends_decls_part_globals [in MetaRocq.Common.Environment]
Environment.on_contexts_over [in MetaRocq.Common.Environment]
Environment.on_contexts [in MetaRocq.Common.Environment]
Environment.on_decls [in MetaRocq.Common.Environment]
Environment.strictly_extends_decls_part [in MetaRocq.Common.Environment]
Environment.strictly_extends_decls_part_globals [in MetaRocq.Common.Environment]
EnvTyping.All_local_rel_size_gen [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_typing_size [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_sorting_size [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_typing [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_typing1 [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_sorting2 [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_sorting1 [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_wfb_term1 [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_wf_term1 [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.on_def_body_size [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.on_def_body_sorting_size [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.on_def_type_size [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.on_def_type_sorting_size [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.on_local_decl [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.Prop_conj [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.Prop_local_conj [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.typing_sort_size1 [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.typing_sort_size [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.typing_sort2 [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.typing_sort1 [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.typing_sort [in MetaRocq.Common.EnvironmentTyping]
eqb_context_gen [in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_term_upto_univ [in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_context_upto_names [in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_term_conv [in MetaRocq.SafeChecker.PCUICSafeChecker]
eqb_term [in MetaRocq.SafeChecker.PCUICSafeConversion]
eqb_ctx [in MetaRocq.SafeChecker.PCUICSafeConversion]
eqt [in MetaRocq.PCUIC.PCUICSN]
eq_termp [in MetaRocq.PCUIC.PCUICCumulativity]
eq_annots [in MetaRocq.PCUIC.PCUICEquality]
eq_context_upto [in MetaRocq.PCUIC.PCUICEquality]
eq_context [in MetaRocq.PCUIC.PCUICEquality]
eq_decl [in MetaRocq.PCUIC.PCUICEquality]
eq_term [in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ [in MetaRocq.PCUIC.PCUICEquality]
eq_context_gen [in MetaRocq.PCUIC.PCUICEquality]
eq_context_upto_names [in MetaRocq.PCUIC.PCUICEquality]
eq_term [in MetaRocq.Template.TermEquality]
eq_term_upto_univ [in MetaRocq.Template.TermEquality]
eq_context_upto_names [in MetaRocq.Template.TermEquality]
eq_term [in MetaRocq.SafeChecker.PCUICEqualityDec]
eq_one_decl [in MetaRocq.PCUIC.PCUICConfluence]
eq_names [in MetaRocq.PCUIC.PCUICContexts]
eq_names [in MetaRocq.PCUIC.PCUICCasesContexts]
eq_inductive [in MetaRocq.Common.Kernames]
eq_kername [in MetaRocq.Common.Kernames]
eq_term_napp [in MetaRocq.PCUIC.PCUICCumulProp]
eq_term [in MetaRocq.SafeChecker.PCUICSafeConversion]
eq_names [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
eval [in MetaRocq.Erasure.EWcbvEval]
eval_pcuic_quotation [in MetaRocq.TemplatePCUIC.Loader]
eval_pcuic_quotation [in MetaRocq.TemplatePCUIC.PCUICTemplateMonad.Core]
expand [in MetaRocq.SafeChecker.PCUICSafeConversion]
| 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) |