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 | (75519 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 | (245 entries) |
Binder 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 | (61331 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 | (144 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 | (89 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 | (236 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 | (6913 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 | (1141 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 | (34 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 | (269 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 | (443 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 | (296 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 | (604 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 | (248 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 | (3386 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 | (140 entries) |
E (constructor)
emptys [in MetaCoq.PCUIC.PCUICSubstitution]emptyslet [in MetaCoq.PCUIC.PCUICSubstitution]
EnvError [in MetaCoq.SafeChecker.PCUICErrors]
EnvError [in MetaCoq.Template.Checker]
Environment.ConstantDecl [in MetaCoq.Template.Environment]
Environment.InductiveDecl [in MetaCoq.Template.Environment]
Environment.on_vdef_alpha [in MetaCoq.Template.Environment]
Environment.on_vass_alpha [in MetaCoq.Template.Environment]
Environment.on_vdef [in MetaCoq.Template.Environment]
Environment.on_vass [in MetaCoq.Template.Environment]
EnvMap.fresh_globals_cons [in MetaCoq.Template.EnvMap]
EnvMap.fresh_globals_empty [in MetaCoq.Template.EnvMap]
EnvTyping.ctx_inst_def [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.ctx_inst_ass [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.ctx_inst_nil [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.localenv_over_cons_def [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.localenv_over_cons_abs [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.localenv_over_nil [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.localenv_cons_def [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.localenv_cons_abs [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.localenv_nil [in MetaCoq.Template.EnvironmentTyping]
eq_Cast [in MetaCoq.Template.TermEquality]
eq_CoFix [in MetaCoq.Template.TermEquality]
eq_Fix [in MetaCoq.Template.TermEquality]
eq_Proj [in MetaCoq.Template.TermEquality]
eq_Case [in MetaCoq.Template.TermEquality]
eq_LetIn [in MetaCoq.Template.TermEquality]
eq_Prod [in MetaCoq.Template.TermEquality]
eq_Lambda [in MetaCoq.Template.TermEquality]
eq_Construct [in MetaCoq.Template.TermEquality]
eq_Ind [in MetaCoq.Template.TermEquality]
eq_Const [in MetaCoq.Template.TermEquality]
eq_App [in MetaCoq.Template.TermEquality]
eq_Sort [in MetaCoq.Template.TermEquality]
eq_Var [in MetaCoq.Template.TermEquality]
eq_Evar [in MetaCoq.Template.TermEquality]
eq_Rel [in MetaCoq.Template.TermEquality]
eq_CoFix [in MetaCoq.PCUIC.PCUICEquality]
eq_Fix [in MetaCoq.PCUIC.PCUICEquality]
eq_Proj [in MetaCoq.PCUIC.PCUICEquality]
eq_Case [in MetaCoq.PCUIC.PCUICEquality]
eq_LetIn [in MetaCoq.PCUIC.PCUICEquality]
eq_Prod [in MetaCoq.PCUIC.PCUICEquality]
eq_Lambda [in MetaCoq.PCUIC.PCUICEquality]
eq_Construct [in MetaCoq.PCUIC.PCUICEquality]
eq_Ind [in MetaCoq.PCUIC.PCUICEquality]
eq_Const [in MetaCoq.PCUIC.PCUICEquality]
eq_App [in MetaCoq.PCUIC.PCUICEquality]
eq_Sort [in MetaCoq.PCUIC.PCUICEquality]
eq_Var [in MetaCoq.PCUIC.PCUICEquality]
eq_Evar [in MetaCoq.PCUIC.PCUICEquality]
eq_Rel [in MetaCoq.PCUIC.PCUICEquality]
erases_deps_tCoFix [in MetaCoq.Erasure.Extract]
erases_deps_tFix [in MetaCoq.Erasure.Extract]
erases_deps_tProj [in MetaCoq.Erasure.Extract]
erases_deps_tCase [in MetaCoq.Erasure.Extract]
erases_deps_tConstruct [in MetaCoq.Erasure.Extract]
erases_deps_tConst [in MetaCoq.Erasure.Extract]
erases_deps_tApp [in MetaCoq.Erasure.Extract]
erases_deps_tLetIn [in MetaCoq.Erasure.Extract]
erases_deps_tLambda [in MetaCoq.Erasure.Extract]
erases_deps_tEvar [in MetaCoq.Erasure.Extract]
erases_deps_tVar [in MetaCoq.Erasure.Extract]
erases_deps_tRel [in MetaCoq.Erasure.Extract]
erases_deps_tBox [in MetaCoq.Erasure.Extract]
erases_global_ind [in MetaCoq.Erasure.Extract]
erases_global_cnst [in MetaCoq.Erasure.Extract]
erases_global_nil [in MetaCoq.Erasure.Extract]
erases_box [in MetaCoq.Erasure.Extract]
erases_tCoFix [in MetaCoq.Erasure.Extract]
erases_tFix [in MetaCoq.Erasure.Extract]
erases_tProj [in MetaCoq.Erasure.Extract]
erases_tCase1 [in MetaCoq.Erasure.Extract]
erases_tConstruct [in MetaCoq.Erasure.Extract]
erases_tConst [in MetaCoq.Erasure.Extract]
erases_tApp [in MetaCoq.Erasure.Extract]
erases_tLetIn [in MetaCoq.Erasure.Extract]
erases_tLambda [in MetaCoq.Erasure.Extract]
erases_tEvar [in MetaCoq.Erasure.Extract]
erases_tVar [in MetaCoq.Erasure.Extract]
erases_tRel [in MetaCoq.Erasure.Extract]
Error [in MetaCoq.Translations.translation_utils]
Error [in MetaCoq.SafeChecker.PCUICSafeConversion]
eval_atom [in MetaCoq.PCUIC.PCUICWcbvEval]
eval_app_cong [in MetaCoq.PCUIC.PCUICWcbvEval]
eval_construct [in MetaCoq.PCUIC.PCUICWcbvEval]
eval_cofix_proj [in MetaCoq.PCUIC.PCUICWcbvEval]
eval_cofix_case [in MetaCoq.PCUIC.PCUICWcbvEval]
eval_fix_value [in MetaCoq.PCUIC.PCUICWcbvEval]
eval_fix [in MetaCoq.PCUIC.PCUICWcbvEval]
eval_proj [in MetaCoq.PCUIC.PCUICWcbvEval]
eval_iota [in MetaCoq.PCUIC.PCUICWcbvEval]
eval_delta [in MetaCoq.PCUIC.PCUICWcbvEval]
eval_zeta [in MetaCoq.PCUIC.PCUICWcbvEval]
eval_beta [in MetaCoq.PCUIC.PCUICWcbvEval]
eval_atom [in MetaCoq.Template.WcbvEval]
eval_app_cong [in MetaCoq.Template.WcbvEval]
eval_construct [in MetaCoq.Template.WcbvEval]
eval_cofix_proj [in MetaCoq.Template.WcbvEval]
eval_cofix_case [in MetaCoq.Template.WcbvEval]
eval_fix_value [in MetaCoq.Template.WcbvEval]
eval_fix [in MetaCoq.Template.WcbvEval]
eval_proj [in MetaCoq.Template.WcbvEval]
eval_iota [in MetaCoq.Template.WcbvEval]
eval_delta [in MetaCoq.Template.WcbvEval]
eval_zeta [in MetaCoq.Template.WcbvEval]
eval_beta [in MetaCoq.Template.WcbvEval]
eval_atom [in MetaCoq.Erasure.EWcbvEval]
eval_app_cong [in MetaCoq.Erasure.EWcbvEval]
eval_construct_block [in MetaCoq.Erasure.EWcbvEval]
eval_construct [in MetaCoq.Erasure.EWcbvEval]
eval_proj_prop [in MetaCoq.Erasure.EWcbvEval]
eval_proj_block [in MetaCoq.Erasure.EWcbvEval]
eval_proj [in MetaCoq.Erasure.EWcbvEval]
eval_delta [in MetaCoq.Erasure.EWcbvEval]
eval_cofix_proj [in MetaCoq.Erasure.EWcbvEval]
eval_cofix_case [in MetaCoq.Erasure.EWcbvEval]
eval_fix' [in MetaCoq.Erasure.EWcbvEval]
eval_fix_value [in MetaCoq.Erasure.EWcbvEval]
eval_fix [in MetaCoq.Erasure.EWcbvEval]
eval_iota_sing [in MetaCoq.Erasure.EWcbvEval]
eval_iota_block [in MetaCoq.Erasure.EWcbvEval]
eval_iota [in MetaCoq.Erasure.EWcbvEval]
eval_zeta [in MetaCoq.Erasure.EWcbvEval]
eval_beta [in MetaCoq.Erasure.EWcbvEval]
eval_box [in MetaCoq.Erasure.EWcbvEval]
evar_red [in MetaCoq.Template.Typing]
evar_pred [in MetaCoq.PCUIC.PCUICParallelReduction]
evar_red [in MetaCoq.PCUIC.PCUICReduction]
expanded_global_cons [in MetaCoq.Template.EtaExpand]
expanded_global_nil [in MetaCoq.Template.EtaExpand]
expanded_tConstruct_app [in MetaCoq.Template.EtaExpand]
expanded_tCoFix [in MetaCoq.Template.EtaExpand]
expanded_tFix [in MetaCoq.Template.EtaExpand]
expanded_tProj [in MetaCoq.Template.EtaExpand]
expanded_tCase [in MetaCoq.Template.EtaExpand]
expanded_tConstruct [in MetaCoq.Template.EtaExpand]
expanded_tInd [in MetaCoq.Template.EtaExpand]
expanded_tConst [in MetaCoq.Template.EtaExpand]
expanded_tApp [in MetaCoq.Template.EtaExpand]
expanded_tLetIn [in MetaCoq.Template.EtaExpand]
expanded_tLambda [in MetaCoq.Template.EtaExpand]
expanded_tProd [in MetaCoq.Template.EtaExpand]
expanded_tCast [in MetaCoq.Template.EtaExpand]
expanded_tSort [in MetaCoq.Template.EtaExpand]
expanded_tEvar [in MetaCoq.Template.EtaExpand]
expanded_tVar [in MetaCoq.Template.EtaExpand]
expanded_tRel_app [in MetaCoq.Template.EtaExpand]
expanded_tRel [in MetaCoq.Template.EtaExpand]
expanded_head_other [in MetaCoq.Erasure.EEtaExpandedFix]
expanded_head_rel [in MetaCoq.Erasure.EEtaExpandedFix]
expanded_head_fix [in MetaCoq.Erasure.EEtaExpandedFix]
expanded_head_construct [in MetaCoq.Erasure.EEtaExpandedFix]
expanded_global_cons [in MetaCoq.Erasure.EEtaExpandedFix]
expanded_global_nil [in MetaCoq.Erasure.EEtaExpandedFix]
expanded_tBox [in MetaCoq.Erasure.EEtaExpandedFix]
expanded_tConstruct_app [in MetaCoq.Erasure.EEtaExpandedFix]
expanded_tCoFix [in MetaCoq.Erasure.EEtaExpandedFix]
expanded_tFix [in MetaCoq.Erasure.EEtaExpandedFix]
expanded_tProj [in MetaCoq.Erasure.EEtaExpandedFix]
expanded_tCase [in MetaCoq.Erasure.EEtaExpandedFix]
expanded_tConst [in MetaCoq.Erasure.EEtaExpandedFix]
expanded_mkApps [in MetaCoq.Erasure.EEtaExpandedFix]
expanded_tLetIn [in MetaCoq.Erasure.EEtaExpandedFix]
expanded_tLambda [in MetaCoq.Erasure.EEtaExpandedFix]
expanded_tEvar [in MetaCoq.Erasure.EEtaExpandedFix]
expanded_tVar [in MetaCoq.Erasure.EEtaExpandedFix]
expanded_tRel_app [in MetaCoq.Erasure.EEtaExpandedFix]
expanded_global_cons [in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_global_nil [in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_tConstruct_app [in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_tCoFix [in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_tFix [in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_tProj [in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_tCase [in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_tInd [in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_tConst [in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_mkApps [in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_tLetIn [in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_tLambda [in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_tProd [in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_tSort [in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_tEvar [in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_tVar [in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_tRel [in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_global_cons [in MetaCoq.Erasure.EEtaExpanded]
expanded_global_nil [in MetaCoq.Erasure.EEtaExpanded]
expanded_tBox [in MetaCoq.Erasure.EEtaExpanded]
expanded_tConstruct_app [in MetaCoq.Erasure.EEtaExpanded]
expanded_tCoFix [in MetaCoq.Erasure.EEtaExpanded]
expanded_tFix [in MetaCoq.Erasure.EEtaExpanded]
expanded_tProj [in MetaCoq.Erasure.EEtaExpanded]
expanded_tCase [in MetaCoq.Erasure.EEtaExpanded]
expanded_tConst [in MetaCoq.Erasure.EEtaExpanded]
expanded_mkApps [in MetaCoq.Erasure.EEtaExpanded]
expanded_tLetIn [in MetaCoq.Erasure.EEtaExpanded]
expanded_tLambda [in MetaCoq.Erasure.EEtaExpanded]
expanded_tEvar [in MetaCoq.Erasure.EEtaExpanded]
expanded_tVar [in MetaCoq.Erasure.EEtaExpanded]
expanded_tRel [in MetaCoq.Erasure.EEtaExpanded]
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 | (75519 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 | (245 entries) |
Binder 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 | (61331 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 | (144 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 | (89 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 | (236 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 | (6913 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 | (1141 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 | (34 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 | (269 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 | (443 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 | (296 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 | (604 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 | (248 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 | (3386 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 | (140 entries) |