| 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
E [module, in MetaCoq.Erasure.Extract]EArities [library]
EAst [library]
EAstUtils [library]
eA:101 [binder, in MetaCoq.PCUIC.utils.PCUICUtils]
ea:141 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
eA:18 [binder, in MetaCoq.PCUIC.utils.PCUICUtils]
eA:59 [binder, in MetaCoq.PCUIC.utils.PCUICUtils]
ecb:1254 [binder, in MetaCoq.Erasure.ErasureFunction]
eckmann_hilton [definition, in MetaCoq.Translations.MiniHoTT]
eckmann_hilton [definition, in MetaCoq.Translations.MiniHoTT_paths]
ecofix_subst_nth [lemma, in MetaCoq.Erasure.Prelim]
EConstructorsAsBlocks [library]
ECSubst [library]
EDeps [library]
EdgeSet_triple [definition, in MetaCoq.Template.common.uGraph]
EdgeSet_pair [definition, in MetaCoq.Template.common.uGraph]
edges:201 [binder, in MetaCoq.SafeChecker.PCUICErrors]
edges:209 [binder, in MetaCoq.Template.common.uGraph]
edges:538 [binder, in MetaCoq.Template.common.uGraph]
edges:539 [binder, in MetaCoq.Template.common.uGraph]
edge_of_constraint [definition, in MetaCoq.Template.common.uGraph]
edge_of_level [definition, in MetaCoq.Template.common.uGraph]
Ee [module, in MetaCoq.Erasure.Prelim]
EEnvFlags [section, in MetaCoq.Erasure.EWellformed]
EEnvFlags [record, in MetaCoq.Erasure.EWellformed]
EEnvFlags [section, in MetaCoq.Erasure.EExtends]
EEnvMap [library]
EEtaExpanded [library]
EEtaExpandedFix [library]
EExtends [library]
efix_subst_nth [lemma, in MetaCoq.Erasure.Prelim]
efl:1 [binder, in MetaCoq.Erasure.EInlineProjections]
efl:1 [binder, in MetaCoq.Erasure.EProgram]
efl:1 [binder, in MetaCoq.Erasure.EExtends]
efl:101 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
efl:102 [binder, in MetaCoq.Erasure.EInlineProjections]
efl:106 [binder, in MetaCoq.Erasure.ETransform]
efl:109 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
efl:11 [binder, in MetaCoq.Erasure.EGenericMapEnv]
efl:111 [binder, in MetaCoq.Erasure.EWellformed]
efl:112 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
efl:113 [binder, in MetaCoq.Erasure.EWellformed]
efl:115 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
efl:118 [binder, in MetaCoq.Erasure.EWellformed]
efl:118 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
efl:1186 [binder, in MetaCoq.Erasure.ErasureFunction]
efl:1195 [binder, in MetaCoq.Erasure.ErasureFunction]
efl:1205 [binder, in MetaCoq.Erasure.ErasureFunction]
efl:1217 [binder, in MetaCoq.Erasure.ErasureFunction]
efl:124 [binder, in MetaCoq.Erasure.EWellformed]
efl:128 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
efl:130 [binder, in MetaCoq.Erasure.EWellformed]
efl:130 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
efl:135 [binder, in MetaCoq.Erasure.EWellformed]
efl:137 [binder, in MetaCoq.Erasure.EInlineProjections]
efl:14 [binder, in MetaCoq.Erasure.EProgram]
efl:140 [binder, in MetaCoq.Erasure.EWellformed]
efl:140 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
efl:142 [binder, in MetaCoq.Erasure.EInlineProjections]
efl:144 [binder, in MetaCoq.Erasure.EWellformed]
efl:145 [binder, in MetaCoq.Erasure.EInlineProjections]
efl:148 [binder, in MetaCoq.Erasure.EInlineProjections]
efl:15 [binder, in MetaCoq.Erasure.ErasureCorrectness]
efl:150 [binder, in MetaCoq.Erasure.EInlineProjections]
efl:152 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
efl:153 [binder, in MetaCoq.Erasure.EInlineProjections]
efl:1534 [binder, in MetaCoq.Erasure.ErasureFunction]
efl:154 [binder, in MetaCoq.Erasure.EInlineProjections]
efl:157 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
efl:158 [binder, in MetaCoq.Erasure.EInlineProjections]
efl:160 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
efl:162 [binder, in MetaCoq.Erasure.EInlineProjections]
efl:163 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
efl:164 [binder, in MetaCoq.Erasure.EEtaExpanded]
efl:165 [binder, in MetaCoq.Erasure.EInlineProjections]
efl:165 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
efl:167 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
efl:170 [binder, in MetaCoq.Erasure.EInlineProjections]
efl:170 [binder, in MetaCoq.Erasure.EEtaExpanded]
efl:171 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
efl:173 [binder, in MetaCoq.Erasure.EInlineProjections]
efl:174 [binder, in MetaCoq.Erasure.EEtaExpanded]
efl:175 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
efl:177 [binder, in MetaCoq.Erasure.EInlineProjections]
efl:178 [binder, in MetaCoq.Erasure.EEtaExpanded]
efl:178 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
efl:183 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
efl:186 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
efl:190 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
efl:2 [binder, in MetaCoq.Erasure.EInlineProjections]
efl:2 [binder, in MetaCoq.Erasure.Erasure]
efl:23 [binder, in MetaCoq.Erasure.EWellformed]
efl:3 [binder, in MetaCoq.Erasure.EProgram]
efl:310 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
efl:312 [binder, in MetaCoq.Erasure.EWcbvEval]
efl:351 [binder, in MetaCoq.Erasure.EWcbvEval]
efl:365 [binder, in MetaCoq.Erasure.ERemoveParams]
efl:369 [binder, in MetaCoq.Erasure.ERemoveParams]
efl:38 [binder, in MetaCoq.Erasure.ETransform]
efl:39 [binder, in MetaCoq.Erasure.EWellformed]
efl:394 [binder, in MetaCoq.Erasure.ERemoveParams]
efl:398 [binder, in MetaCoq.Erasure.ERemoveParams]
efl:401 [binder, in MetaCoq.Erasure.ERemoveParams]
efl:402 [binder, in MetaCoq.Erasure.ERemoveParams]
efl:419 [binder, in MetaCoq.Erasure.ERemoveParams]
efl:424 [binder, in MetaCoq.Erasure.ERemoveParams]
efl:429 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
efl:429 [binder, in MetaCoq.Erasure.ERemoveParams]
efl:433 [binder, in MetaCoq.Erasure.ERemoveParams]
efl:435 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
efl:436 [binder, in MetaCoq.Erasure.ERemoveParams]
efl:438 [binder, in MetaCoq.Erasure.ERemoveParams]
efl:440 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
efl:440 [binder, in MetaCoq.Erasure.ERemoveParams]
efl:444 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
efl:444 [binder, in MetaCoq.Erasure.ERemoveParams]
efl:449 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
efl:449 [binder, in MetaCoq.Erasure.ERemoveParams]
efl:451 [binder, in MetaCoq.Erasure.ERemoveParams]
efl:46 [binder, in MetaCoq.Erasure.EWellformed]
efl:48 [binder, in MetaCoq.Erasure.EWellformed]
efl:48 [binder, in MetaCoq.Erasure.ETransform]
efl:491 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
efl:496 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
efl:5 [binder, in MetaCoq.Erasure.Erasure]
efl:52 [binder, in MetaCoq.Erasure.ETransform]
efl:53 [binder, in MetaCoq.Erasure.EWellformed]
efl:55 [binder, in MetaCoq.Erasure.EInlineProjections]
efl:551 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
efl:560 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
efl:59 [binder, in MetaCoq.Erasure.EWellformed]
efl:6 [binder, in MetaCoq.Erasure.EInlineProjections]
efl:63 [binder, in MetaCoq.Erasure.ETransform]
efl:68 [binder, in MetaCoq.Erasure.EInlineProjections]
efl:74 [binder, in MetaCoq.Erasure.ETransform]
efl:76 [binder, in MetaCoq.Erasure.EInlineProjections]
efl:79 [binder, in MetaCoq.Erasure.EInlineProjections]
efl:82 [binder, in MetaCoq.Erasure.EInlineProjections]
efl:84 [binder, in MetaCoq.Erasure.ETransform]
efl:85 [binder, in MetaCoq.Erasure.EInlineProjections]
efl:88 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
efl:96 [binder, in MetaCoq.Erasure.ETransform]
efl:98 [binder, in MetaCoq.Erasure.EInlineProjections]
EGenericMapEnv [library]
EGlobalEnv [library]
EInduction [library]
einfering_sort_isType [lemma, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
EInlineProjections [library]
eisadj [projection, in MetaCoq.Translations.MiniHoTT]
eisadj [projection, in MetaCoq.Translations.MiniHoTT_paths]
eisretr [projection, in MetaCoq.Translations.MiniHoTT]
eisretr [projection, in MetaCoq.Translations.MiniHoTT_paths]
eissect [projection, in MetaCoq.Translations.MiniHoTT]
eissect [projection, in MetaCoq.Translations.MiniHoTT_paths]
ei:1477 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
ei:1950 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
ei:357 [binder, in MetaCoq.Template.common.uGraph]
ei:373 [binder, in MetaCoq.Template.common.uGraph]
ei:374 [binder, in MetaCoq.Template.common.uGraph]
ei:377 [binder, in MetaCoq.Template.common.uGraph]
ei:380 [binder, in MetaCoq.Template.common.uGraph]
ei:384 [binder, in MetaCoq.Template.common.uGraph]
ei:387 [binder, in MetaCoq.Template.common.uGraph]
ei:389 [binder, in MetaCoq.Template.common.uGraph]
ei:392 [binder, in MetaCoq.Template.common.uGraph]
ELiftSubst [library]
elimP [lemma, in MetaCoq.Template.utils.ReflectEq]
elims:69 [binder, in MetaCoq.Erasure.EPretty]
elimT [lemma, in MetaCoq.Template.utils.MCReflect]
elim_restriction_works_proj [lemma, in MetaCoq.PCUIC.PCUICElimination]
elim_restriction_works_proj_kelim1 [lemma, in MetaCoq.PCUIC.PCUICElimination]
elim_restriction_works [lemma, in MetaCoq.PCUIC.PCUICElimination]
elim_restriction_works_kelim [lemma, in MetaCoq.PCUIC.PCUICElimination]
elim_sort_intype [lemma, in MetaCoq.PCUIC.PCUICElimination]
elim_restriction_works_kelim1 [lemma, in MetaCoq.PCUIC.PCUICElimination]
elim_inspect [lemma, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
Elim' [section, in MetaCoq.Erasure.EArities]
Elim'.Hcf [variable, in MetaCoq.Erasure.EArities]
Elim'.Hcf' [variable, in MetaCoq.Erasure.EArities]
elookup_env_cons_disc [lemma, in MetaCoq.Erasure.ErasureFunction]
elookup_env_cons_fresh [lemma, in MetaCoq.Erasure.EGlobalEnv]
elt:512 [binder, in MetaCoq.Template.EnvironmentTyping]
emax [definition, in MetaCoq.Template.BasicAst]
embed:1003 [binder, in MetaCoq.Template.utils.wGraph]
embed:1156 [binder, in MetaCoq.Template.utils.wGraph]
emkApps_snoc [lemma, in MetaCoq.Erasure.Prelim]
emptys [constructor, in MetaCoq.PCUIC.PCUICSubstitution]
emptyslet [constructor, in MetaCoq.PCUIC.PCUICSubstitution]
emptyTC [definition, in MetaCoq.Translations.translation_utils]
empty_contextset_subset [lemma, in MetaCoq.Template.Universes]
empty_ext [definition, in MetaCoq.PCUIC.utils.PCUICAstUtils]
empty_trans_env [definition, in MetaCoq.PCUIC.TemplateToPCUIC]
empty:90 [binder, in MetaCoq.Template.common.uGraph]
Env [module, in MetaCoq.Template.Ast]
EnvCheck [inductive, in MetaCoq.SafeChecker.PCUICErrors]
EnvCheck [section, in MetaCoq.SafeChecker.PCUICErrors]
EnvCheck [inductive, in MetaCoq.Template.Checker]
envcheck_monad_exc [instance, in MetaCoq.SafeChecker.PCUICErrors]
envcheck_monad [instance, in MetaCoq.SafeChecker.PCUICErrors]
EnvCheck_wf_env_ext [definition, in MetaCoq.SafeChecker.SafeTemplateChecker]
envcheck_monad [instance, in MetaCoq.Template.Checker]
EnvCheck_X_env_ext_type [definition, in MetaCoq.SafeChecker.PCUICSafeChecker]
EnvError [constructor, in MetaCoq.SafeChecker.PCUICErrors]
EnvError [constructor, in MetaCoq.Template.Checker]
Environment [module, in MetaCoq.Template.Environment]
Environment [library]
EnvironmentSig [module, in MetaCoq.Template.Environment]
EnvironmentTyping [library]
Environment.add_global_decl [definition, in MetaCoq.Template.Environment]
Environment.All_decls_to_alpha [lemma, in MetaCoq.Template.Environment]
Environment.All_decls_alpha_impl [lemma, in MetaCoq.Template.Environment]
Environment.All_decls_impl [lemma, in MetaCoq.Template.Environment]
Environment.All_decls_alpha [inductive, in MetaCoq.Template.Environment]
Environment.All_decls [inductive, in MetaCoq.Template.Environment]
Environment.All2_fold_over [definition, in MetaCoq.Template.Environment]
Environment.app_context_length [lemma, in MetaCoq.Template.Environment]
Environment.app_context_cons [lemma, in MetaCoq.Template.Environment]
Environment.app_context_assoc [lemma, in MetaCoq.Template.Environment]
Environment.app_context_nil_l [lemma, in MetaCoq.Template.Environment]
Environment.app_context [definition, in MetaCoq.Template.Environment]
Environment.arities_context_length [lemma, in MetaCoq.Template.Environment]
Environment.arities_context [definition, in MetaCoq.Template.Environment]
Environment.ConstantDecl [constructor, in MetaCoq.Template.Environment]
Environment.constant_body [record, in MetaCoq.Template.Environment]
Environment.constructor_body [record, in MetaCoq.Template.Environment]
Environment.context [definition, in MetaCoq.Template.Environment]
Environment.context_assumptions_lift_context [lemma, in MetaCoq.Template.Environment]
Environment.context_assumptions_subst_context [lemma, in MetaCoq.Template.Environment]
Environment.context_assumptions_subst_instance [lemma, in MetaCoq.Template.Environment]
Environment.context_assumptions_mapi [lemma, in MetaCoq.Template.Environment]
Environment.context_assumptions_app [lemma, in MetaCoq.Template.Environment]
Environment.context_assumptions_map [lemma, in MetaCoq.Template.Environment]
Environment.context_assumptions_length_bound [lemma, in MetaCoq.Template.Environment]
Environment.context_assumptions_fold [lemma, in MetaCoq.Template.Environment]
Environment.context_assumptions [definition, in MetaCoq.Template.Environment]
Environment.context_decl [abbreviation, in MetaCoq.Template.Environment]
Environment.cstr_arity [projection, in MetaCoq.Template.Environment]
Environment.cstr_type [projection, in MetaCoq.Template.Environment]
Environment.cstr_indices [projection, in MetaCoq.Template.Environment]
Environment.cstr_args [projection, in MetaCoq.Template.Environment]
Environment.cstr_name [projection, in MetaCoq.Template.Environment]
Environment.cst_relevance [projection, in MetaCoq.Template.Environment]
Environment.cst_universes [projection, in MetaCoq.Template.Environment]
Environment.cst_body [projection, in MetaCoq.Template.Environment]
Environment.cst_type [projection, in MetaCoq.Template.Environment]
Environment.declarations [projection, in MetaCoq.Template.Environment]
Environment.empty_ext [definition, in MetaCoq.Template.Environment]
Environment.empty_global_env [definition, in MetaCoq.Template.Environment]
Environment.eta_global_env [lemma, in MetaCoq.Template.Environment]
Environment.expand_lets_ctx_length [lemma, in MetaCoq.Template.Environment]
Environment.expand_lets_k_ctx_length [lemma, in MetaCoq.Template.Environment]
Environment.expand_lets_ctx [definition, in MetaCoq.Template.Environment]
Environment.expand_lets_k_ctx [definition, in MetaCoq.Template.Environment]
Environment.expand_lets [definition, in MetaCoq.Template.Environment]
Environment.expand_lets_k [definition, in MetaCoq.Template.Environment]
Environment.extended_subst_length [lemma, in MetaCoq.Template.Environment]
Environment.extended_subst [definition, in MetaCoq.Template.Environment]
Environment.extends [definition, in MetaCoq.Template.Environment]
Environment.extends_refl [lemma, in MetaCoq.Template.Environment]
Environment.extends_decls_refl [instance, in MetaCoq.Template.Environment]
Environment.extends_decls_extends [instance, in MetaCoq.Template.Environment]
Environment.extends_decls [definition, in MetaCoq.Template.Environment]
Environment.fix_context [definition, in MetaCoq.Template.Environment]
Environment.fst_ctx [definition, in MetaCoq.Template.Environment]
Environment.global_env_ext [definition, in MetaCoq.Template.Environment]
Environment.global_env [record, in MetaCoq.Template.Environment]
Environment.global_declarations [definition, in MetaCoq.Template.Environment]
Environment.global_decl [inductive, in MetaCoq.Template.Environment]
Environment.InductiveDecl [constructor, in MetaCoq.Template.Environment]
Environment.ind_projs_map [lemma, in MetaCoq.Template.Environment]
Environment.ind_pars_map [lemma, in MetaCoq.Template.Environment]
Environment.ind_ctors_map [lemma, in MetaCoq.Template.Environment]
Environment.ind_type_map [lemma, in MetaCoq.Template.Environment]
Environment.ind_variance [projection, in MetaCoq.Template.Environment]
Environment.ind_universes [projection, in MetaCoq.Template.Environment]
Environment.ind_bodies [projection, in MetaCoq.Template.Environment]
Environment.ind_params [projection, in MetaCoq.Template.Environment]
Environment.ind_npars [projection, in MetaCoq.Template.Environment]
Environment.ind_finite [projection, in MetaCoq.Template.Environment]
Environment.ind_relevance [projection, in MetaCoq.Template.Environment]
Environment.ind_projs [projection, in MetaCoq.Template.Environment]
Environment.ind_ctors [projection, in MetaCoq.Template.Environment]
Environment.ind_kelim [projection, in MetaCoq.Template.Environment]
Environment.ind_type [projection, in MetaCoq.Template.Environment]
Environment.ind_sort [projection, in MetaCoq.Template.Environment]
Environment.ind_indices [projection, in MetaCoq.Template.Environment]
Environment.ind_name [projection, in MetaCoq.Template.Environment]
Environment.is_assumption_context [definition, in MetaCoq.Template.Environment]
Environment.it_mkProd_or_LetIn_app [lemma, in MetaCoq.Template.Environment]
Environment.it_mkProd_or_LetIn [definition, in MetaCoq.Template.Environment]
Environment.it_mkLambda_or_LetIn [definition, in MetaCoq.Template.Environment]
Environment.lift_context_length [lemma, in MetaCoq.Template.Environment]
Environment.lift_context_alt [lemma, in MetaCoq.Template.Environment]
Environment.lift_context [definition, in MetaCoq.Template.Environment]
Environment.lift_decl [definition, in MetaCoq.Template.Environment]
Environment.lookup_env [definition, in MetaCoq.Template.Environment]
Environment.lookup_global [definition, in MetaCoq.Template.Environment]
Environment.map_mutual_inductive_body [definition, in MetaCoq.Template.Environment]
Environment.map_cst_body [lemma, in MetaCoq.Template.Environment]
Environment.map_cst_type [lemma, in MetaCoq.Template.Environment]
Environment.map_constant_body [definition, in MetaCoq.Template.Environment]
Environment.map_one_inductive_body [definition, in MetaCoq.Template.Environment]
Environment.map_projection_body [definition, in MetaCoq.Template.Environment]
Environment.map_constructor_body [definition, in MetaCoq.Template.Environment]
Environment.mkLambda_or_LetIn [definition, in MetaCoq.Template.Environment]
Environment.mkProd_or_LetIn [definition, in MetaCoq.Template.Environment]
Environment.mutual_inductive_body [record, in MetaCoq.Template.Environment]
Environment.nth_error_lt [lemma, in MetaCoq.Template.Environment]
Environment.nth_error_ge [lemma, in MetaCoq.Template.Environment]
Environment.nth_error_fold_context_k_eq [lemma, in MetaCoq.Template.Environment]
Environment.nth_error_fold_context_k [lemma, in MetaCoq.Template.Environment]
Environment.nth_error_app_context_lt [lemma, in MetaCoq.Template.Environment]
Environment.nth_error_app_context_ge [lemma, in MetaCoq.Template.Environment]
Environment.one_inductive_body [record, in MetaCoq.Template.Environment]
Environment.on_contexts_over [abbreviation, in MetaCoq.Template.Environment]
Environment.on_contexts [abbreviation, in MetaCoq.Template.Environment]
Environment.on_decls [abbreviation, in MetaCoq.Template.Environment]
Environment.on_vdef_alpha [constructor, in MetaCoq.Template.Environment]
Environment.on_vass_alpha [constructor, in MetaCoq.Template.Environment]
Environment.on_vdef [constructor, in MetaCoq.Template.Environment]
Environment.on_vass [constructor, in MetaCoq.Template.Environment]
Environment.program [definition, in MetaCoq.Template.Environment]
Environment.projection_body [record, in MetaCoq.Template.Environment]
Environment.projs [definition, in MetaCoq.Template.Environment]
Environment.projs_length [lemma, in MetaCoq.Template.Environment]
Environment.proj_type [projection, in MetaCoq.Template.Environment]
Environment.proj_relevance [projection, in MetaCoq.Template.Environment]
Environment.proj_name [projection, in MetaCoq.Template.Environment]
Environment.reln [definition, in MetaCoq.Template.Environment]
Environment.reln_alt_eq [lemma, in MetaCoq.Template.Environment]
Environment.reln_alt [definition, in MetaCoq.Template.Environment]
Environment.reln_list_lift_above [lemma, in MetaCoq.Template.Environment]
Environment.reln_fold [lemma, in MetaCoq.Template.Environment]
Environment.set_binder_name [definition, in MetaCoq.Template.Environment]
Environment.smash_context_app [lemma, in MetaCoq.Template.Environment]
Environment.smash_context_length [lemma, in MetaCoq.Template.Environment]
Environment.smash_context [definition, in MetaCoq.Template.Environment]
Environment.subst_instance_length [lemma, in MetaCoq.Template.Environment]
Environment.subst_instance_context [instance, in MetaCoq.Template.Environment]
Environment.subst_instance_decl [instance, in MetaCoq.Template.Environment]
Environment.subst_telescope [definition, in MetaCoq.Template.Environment]
Environment.subst_context_snoc [lemma, in MetaCoq.Template.Environment]
Environment.subst_context_alt [lemma, in MetaCoq.Template.Environment]
Environment.subst_context_nil [lemma, in MetaCoq.Template.Environment]
Environment.subst_context_length [lemma, in MetaCoq.Template.Environment]
Environment.subst_decl [definition, in MetaCoq.Template.Environment]
Environment.subst_context [definition, in MetaCoq.Template.Environment]
Environment.to_extended_list_k_cons [lemma, in MetaCoq.Template.Environment]
Environment.to_extended_list_lift_above [lemma, in MetaCoq.Template.Environment]
Environment.to_extended_list_k_spec [lemma, in MetaCoq.Template.Environment]
Environment.to_extended_list [definition, in MetaCoq.Template.Environment]
Environment.to_extended_list_k [definition, in MetaCoq.Template.Environment]
Environment.typ_or_sort [definition, in MetaCoq.Template.Environment]
Environment.universes [projection, in MetaCoq.Template.Environment]
Environment.vass [definition, in MetaCoq.Template.Environment]
Environment.vdef [definition, in MetaCoq.Template.Environment]
_ ,,, _ [notation, in MetaCoq.Template.Environment]
EnvMap [module, in MetaCoq.Template.EnvMap]
EnvMap [library]
EnvMap.add [definition, in MetaCoq.Template.EnvMap]
EnvMap.empty [definition, in MetaCoq.Template.EnvMap]
EnvMap.equal [definition, in MetaCoq.Template.EnvMap]
EnvMap.fold_left_cons [lemma, in MetaCoq.Template.EnvMap]
EnvMap.fresh_globals_cons [constructor, in MetaCoq.Template.EnvMap]
EnvMap.fresh_globals_empty [constructor, in MetaCoq.Template.EnvMap]
EnvMap.fresh_globals [inductive, in MetaCoq.Template.EnvMap]
EnvMap.fresh_global [definition, in MetaCoq.Template.EnvMap]
EnvMap.gso [lemma, in MetaCoq.Template.EnvMap]
EnvMap.gss [lemma, in MetaCoq.Template.EnvMap]
EnvMap.lookup [definition, in MetaCoq.Template.EnvMap]
EnvMap.lookup_spec [lemma, in MetaCoq.Template.EnvMap]
EnvMap.lookup_global [definition, in MetaCoq.Template.EnvMap]
EnvMap.lookup_add_other [lemma, in MetaCoq.Template.EnvMap]
EnvMap.lookup_add [lemma, in MetaCoq.Template.EnvMap]
EnvMap.of_global_env_cons [lemma, in MetaCoq.Template.EnvMap]
EnvMap.of_global_env [definition, in MetaCoq.Template.EnvMap]
EnvMap.Poly [section, in MetaCoq.Template.EnvMap]
EnvMap.remove [definition, in MetaCoq.Template.EnvMap]
EnvMap.remove_add_o [lemma, in MetaCoq.Template.EnvMap]
EnvMap.remove_add_eq [lemma, in MetaCoq.Template.EnvMap]
EnvMap.repr [definition, in MetaCoq.Template.EnvMap]
EnvMap.repr_add [lemma, in MetaCoq.Template.EnvMap]
EnvMap.repr_global_env [lemma, in MetaCoq.Template.EnvMap]
EnvMap.t [definition, in MetaCoq.Template.EnvMap]
EnvMap.unfold_equal [lemma, in MetaCoq.Template.EnvMap]
EnvTyping [module, in MetaCoq.Template.EnvironmentTyping]
EnvTypingSig [module, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_rel_sorting_size [definition, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_env_sorting_size [definition, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_rel_size [definition, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_env_size [definition, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_env_size_app [lemma, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_rel_size_gen [abbreviation, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_env_size_pos [lemma, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_env_size_gen [definition, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_env_size [section, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_env_over_sorting [definition, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_env_over [definition, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_env_over_gen [inductive, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_rel_app [lemma, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_app_rel [lemma, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_local_rel [lemma, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_rel_local [lemma, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_rel_def [definition, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_rel_abs [definition, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_rel_nil [definition, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_rel [definition, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_env_rel [section, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_env_skipn [lemma, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_env_impl_ind [lemma, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_env_impl [lemma, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_env_fold [lemma, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_env [inductive, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.Bidirectional [section, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.ctx_inst_impl [lemma, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.ctx_inst_def [constructor, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.ctx_inst_ass [constructor, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.ctx_inst_nil [constructor, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.ctx_inst [inductive, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.infer_sort_size [abbreviation, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.infer_typing_sort_impl [lemma, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.infer_sort_impl [lemma, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.infer_sort [definition, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.lift_sorting_size [definition, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.lift_typing_size [definition, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.lift_judgment_size [definition, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.lift_judgment_size [section, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.lift_typing_impl [lemma, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.lift_typing2 [definition, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.lift_sorting [definition, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.lift_typing [definition, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.lift_wf_term [definition, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.lift_judgment_impl [lemma, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.lift_judgment [definition, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.localenv_over_cons_def [constructor, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.localenv_over_cons_abs [constructor, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.localenv_over_nil [constructor, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.localenv_cons_def [constructor, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.localenv_cons_abs [constructor, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.localenv_nil [constructor, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.on_def_body [definition, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.on_def_type [definition, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.on_local_decl [definition, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.Prop_conj [abbreviation, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.Regular [section, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.TypeCtxInst [section, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.TypeLocal [section, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.TypeLocalOver [section, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.typing_sort_size [abbreviation, in MetaCoq.Template.EnvironmentTyping]
EnvTyping.typing_sort [abbreviation, in MetaCoq.Template.EnvironmentTyping]
env_prop_bd [definition, in MetaCoq.PCUIC.Bidirectional.BDTyping]
env_eq [lemma, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
env_prop_sigma [lemma, in MetaCoq.Template.Typing]
env_prop_wf_local [lemma, in MetaCoq.Template.Typing]
env_prop_typing [lemma, in MetaCoq.Template.Typing]
env_prop [definition, in MetaCoq.Template.Typing]
env_flags_blocks [definition, in MetaCoq.Erasure.EConstructorsAsBlocks]
env_flags [definition, in MetaCoq.Erasure.EConstructorsAsBlocks]
env_error [inductive, in MetaCoq.SafeChecker.PCUICErrors]
env_error [inductive, in MetaCoq.Template.Checker]
env_prop_sigma [lemma, in MetaCoq.PCUIC.PCUICTyping]
env_prop_wf_local [lemma, in MetaCoq.PCUIC.PCUICTyping]
env_prop_typing [lemma, in MetaCoq.PCUIC.PCUICTyping]
env_prop [definition, in MetaCoq.PCUIC.PCUICTyping]
env:3 [binder, in MetaCoq.Template.EnvMap]
env:352 [binder, in MetaCoq.PCUIC.PCUICEquality]
env:372 [binder, in MetaCoq.Template.Checker]
env:418 [binder, in MetaCoq.Template.Checker]
env:54 [binder, in MetaCoq.PCUIC.TemplateToPCUIC]
env:56 [binder, in MetaCoq.PCUIC.TemplateToPCUIC]
env:6 [binder, in MetaCoq.Template.EnvMap]
env:69 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
env:8 [binder, in MetaCoq.Template.EnvMap]
EOptimizePropDiscr [library]
eo:1102 [binder, in MetaCoq.Template.utils.wGraph]
EPretty [library]
eprogram [definition, in MetaCoq.Erasure.EProgram]
EProgram [library]
eprogram_env [definition, in MetaCoq.Erasure.EProgram]
ep:202 [binder, in MetaCoq.Erasure.ErasureFunction]
eqarglen:360 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
eqarglen:361 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
eqA:57 [binder, in MetaCoq.Template.utils.ReflectEq]
eqA:65 [binder, in MetaCoq.Template.utils.ReflectEq]
eqA:87 [binder, in MetaCoq.Template.utils.ReflectEq]
eqA:97 [binder, in MetaCoq.Template.utils.ReflectEq]
eqb [definition, in MetaCoq.Template.utils.ByteCompare]
eqb [projection, in MetaCoq.Template.utils.ReflectEq]
eqbindices:366 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
eqbpars:365 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
eqbrs_refl [instance, in MetaCoq.PCUIC.PCUICConversion]
eqb_true_iff [lemma, in MetaCoq.Template.Universes]
eqb_binder_annot [definition, in MetaCoq.Template.BasicAst]
eqb_annot_reflect [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
eqb_compare [definition, in MetaCoq.Template.utils.ByteCompareSpec]
eqb_univ_instance:17 [binder, in MetaCoq.Template.Ast]
eqb_predicate [definition, in MetaCoq.Template.Ast]
eqb_univ_instance [definition, in MetaCoq.Template.common.uGraph]
eqb_list [definition, in MetaCoq.Template.utils.ReflectEq]
eqb_refl [lemma, in MetaCoq.Template.utils.ReflectEq]
eqb_eq [lemma, in MetaCoq.Template.utils.ReflectEq]
eqb_specT [lemma, in MetaCoq.Template.utils.ReflectEq]
eqb_spec [projection, in MetaCoq.Template.utils.ReflectEq]
eqb_predicate [definition, in MetaCoq.PCUIC.PCUICAst]
eqb_univ_instance:252 [binder, in MetaCoq.PCUIC.PCUICAst]
eqb_predicate_gen [definition, in MetaCoq.PCUIC.PCUICAst]
eqb_universe_instance_complete [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
eqb_universe_instance_spec [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
eqb_universe_instance [definition, in MetaCoq.SafeChecker.PCUICSafeConversion]
eqb_universe_instance_gen [definition, in MetaCoq.SafeChecker.PCUICSafeConversion]
eqb_term_stack [definition, in MetaCoq.SafeChecker.PCUICSafeConversion]
eqb_term [abbreviation, in MetaCoq.SafeChecker.PCUICSafeConversion]
eqb_ctx [abbreviation, in MetaCoq.SafeChecker.PCUICSafeConversion]
eqb_Variance [definition, in MetaCoq.Template.Reflect]
eqb_allowed_eliminations [definition, in MetaCoq.Template.Reflect]
eqb_universes_decl [definition, in MetaCoq.Template.Reflect]
eqb_ConstraintType [definition, in MetaCoq.Template.Reflect]
eqb_recursivity_kind [definition, in MetaCoq.Template.Reflect]
eqb_context_decl [definition, in MetaCoq.Template.Reflect]
eqb_case_info [definition, in MetaCoq.Template.Reflect]
eqb_ctx [instance, in MetaCoq.Template.ReflectAst]
eqb_global_decl [definition, in MetaCoq.PCUIC.Syntax.PCUICReflect]
eqb_mutual_inductive_body [definition, in MetaCoq.PCUIC.Syntax.PCUICReflect]
eqb_one_inductive_body [definition, in MetaCoq.PCUIC.Syntax.PCUICReflect]
eqb_projection_body [definition, in MetaCoq.PCUIC.Syntax.PCUICReflect]
eqb_constructor_body [definition, in MetaCoq.PCUIC.Syntax.PCUICReflect]
eqb_constant_body [definition, in MetaCoq.PCUIC.Syntax.PCUICReflect]
eqb_context_decl [definition, in MetaCoq.PCUIC.Syntax.PCUICReflect]
eqb_predicate [definition, in MetaCoq.PCUIC.Syntax.PCUICReflect]
eqb_ctx [instance, in MetaCoq.PCUIC.Syntax.PCUICReflect]
eqb_term_reflect [instance, in MetaCoq.PCUIC.Syntax.PCUICReflect]
eqb_term [definition, in MetaCoq.PCUIC.Syntax.PCUICReflect]
eqb_term_conv [abbreviation, in MetaCoq.SafeChecker.PCUICSafeChecker]
eqb_global_decl [definition, in MetaCoq.Erasure.EReflect]
eqb_mutual_inductive_body [definition, in MetaCoq.Erasure.EReflect]
eqb_one_inductive_body [definition, in MetaCoq.Erasure.EReflect]
eqb_projection_body [definition, in MetaCoq.Erasure.EReflect]
eqb_constructor_body [definition, in MetaCoq.Erasure.EReflect]
eqb_constant_body [definition, in MetaCoq.Erasure.EReflect]
eqb_opt_term [definition, in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_ctx_spec [lemma, in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_term_refl [lemma, in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_term_spec [lemma, in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_term [definition, in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_termp [definition, in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_termp_napp_spec [lemma, in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_termp_napp [definition, in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_ctx [definition, in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_ctx_gen_proper [definition, in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_binder_annot_spec [lemma, in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_ctx_gen [definition, in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_term_upto_univ_refl [lemma, in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_term_upto_univ_proper [definition, in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_term_upto_univ_impl [lemma, in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_univ_reflect [definition, in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_annots_reflect [lemma, in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_annots_spec [lemma, in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_annot_refl [lemma, in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_annot_reflect [lemma, in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_annot_spec [lemma, in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_termp_napp_gen [definition, in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_term_upto_univ [abbreviation, in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_term_upto_univ_napp [definition, in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_binder_annots [definition, in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb:238 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
eqb:284 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb:315 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb:423 [binder, in MetaCoq.Template.EnvironmentTyping]
eqB:88 [binder, in MetaCoq.Template.utils.ReflectEq]
eqB:98 [binder, in MetaCoq.Template.utils.ReflectEq]
eqci:2396 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
eqdecl:253 [binder, in MetaCoq.PCUIC.PCUICAst]
eqdec_binder_annot [instance, in MetaCoq.Template.BasicAst]
EqDec_stack_entry [instance, in MetaCoq.PCUIC.Syntax.PCUICPosition]
EqDec_branch_hole [instance, in MetaCoq.PCUIC.Syntax.PCUICPosition]
EqDec_predicate_hole [instance, in MetaCoq.PCUIC.Syntax.PCUICPosition]
EqDec_context_decl_hole [instance, in MetaCoq.PCUIC.Syntax.PCUICPosition]
EqDec_def_hole [instance, in MetaCoq.PCUIC.Syntax.PCUICPosition]
EqDec_ReflectEq [definition, in MetaCoq.Template.utils.ReflectEq]
EqDec_term [instance, in MetaCoq.Template.ReflectAst]
EqDec_term [instance, in MetaCoq.PCUIC.Syntax.PCUICReflect]
EqDec_term [instance, in MetaCoq.Erasure.EReflect]
eqhd:569 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
eqindices:990 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
eqlu':250 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
eqlu':263 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
eqlu':75 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
eqlu:249 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
eqlu:262 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
eqlu:74 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
eqna:237 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
eqna:242 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
eqna:414 [binder, in MetaCoq.Template.EnvironmentTyping]
eqna:422 [binder, in MetaCoq.Template.EnvironmentTyping]
eqpars:359 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
eqpars:989 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
eqr:334 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
eqr:551 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
eqsort:988 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
eqt [abbreviation, in MetaCoq.PCUIC.PCUICSN]
eqt [definition, in MetaCoq.SafeChecker.PCUICSafeConversion]
eqterm:18 [binder, in MetaCoq.Template.Ast]
eqterm:254 [binder, in MetaCoq.PCUIC.PCUICAst]
eqterm:257 [binder, in MetaCoq.PCUIC.PCUICAst]
eqterm:379 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
eqterm:42 [binder, in MetaCoq.Template.Reflect]
eqt_refl [instance, in MetaCoq.SafeChecker.PCUICSafeConversion]
eqt_eqterm [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
eqt:415 [binder, in MetaCoq.Template.EnvironmentTyping]
eqt:424 [binder, in MetaCoq.Template.EnvironmentTyping]
EqualityDec [section, in MetaCoq.SafeChecker.PCUICEqualityDec]
EqualityLemmas [section, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
Equal_graph_edges [lemma, in MetaCoq.Template.common.uGraph]
equal_graph_equiv [instance, in MetaCoq.Template.common.uGraph]
Equal_graph [definition, in MetaCoq.Template.common.uGraph]
equal_subst_instance_cstrs_mono [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
Equiv [record, in MetaCoq.Translations.MiniHoTT]
Equiv [record, in MetaCoq.Translations.MiniHoTT_paths]
equiv [definition, in MetaCoq.Translations.times_bool_fun2]
equiv [definition, in MetaCoq.Translations.param_generous_packed]
EquivInverse [section, in MetaCoq.Translations.MiniHoTT]
EquivInverse [section, in MetaCoq.Translations.MiniHoTT_paths]
EquivTransport [section, in MetaCoq.Translations.MiniHoTT]
EquivTransport [section, in MetaCoq.Translations.MiniHoTT_paths]
equiv_reflectT [lemma, in MetaCoq.Template.utils.MCReflect]
equiv_sigma_assoc [definition, in MetaCoq.Translations.MiniHoTT]
equiv_contr_sigma [definition, in MetaCoq.Translations.MiniHoTT]
equiv_sigma_contr [definition, in MetaCoq.Translations.MiniHoTT]
equiv_functor_sigma_id [definition, in MetaCoq.Translations.MiniHoTT]
equiv_functor_sigma' [definition, in MetaCoq.Translations.MiniHoTT]
equiv_functor_sigma [definition, in MetaCoq.Translations.MiniHoTT]
equiv_path_sigma_contra [definition, in MetaCoq.Translations.MiniHoTT]
equiv_path_sigma [definition, in MetaCoq.Translations.MiniHoTT]
equiv_flip [definition, in MetaCoq.Translations.MiniHoTT]
equiv_contr_forall [definition, in MetaCoq.Translations.MiniHoTT]
equiv_functor_forall_covariant_compose [definition, in MetaCoq.Translations.MiniHoTT]
equiv_functor_forall_covariant [definition, in MetaCoq.Translations.MiniHoTT]
equiv_functor_forall_pf [definition, in MetaCoq.Translations.MiniHoTT]
equiv_functor_forall_pb [definition, in MetaCoq.Translations.MiniHoTT]
equiv_functor_forall_id [definition, in MetaCoq.Translations.MiniHoTT]
equiv_functor_forall' [definition, in MetaCoq.Translations.MiniHoTT]
equiv_functor_forall [definition, in MetaCoq.Translations.MiniHoTT]
equiv_path_forall [definition, in MetaCoq.Translations.MiniHoTT]
equiv_apD10 [definition, in MetaCoq.Translations.MiniHoTT]
equiv_paths_ind [definition, in MetaCoq.Translations.MiniHoTT]
equiv_moveL_equiv_V [definition, in MetaCoq.Translations.MiniHoTT]
equiv_moveL_equiv_M [definition, in MetaCoq.Translations.MiniHoTT]
equiv_moveR_equiv_V [definition, in MetaCoq.Translations.MiniHoTT]
equiv_moveR_equiv_M [definition, in MetaCoq.Translations.MiniHoTT]
equiv_moveL_transport_p [definition, in MetaCoq.Translations.MiniHoTT]
equiv_moveL_transport_V [definition, in MetaCoq.Translations.MiniHoTT]
equiv_moveR_transport_V [definition, in MetaCoq.Translations.MiniHoTT]
equiv_moveR_transport_p [definition, in MetaCoq.Translations.MiniHoTT]
equiv_moveL_pV [definition, in MetaCoq.Translations.MiniHoTT]
equiv_moveL_Vp [definition, in MetaCoq.Translations.MiniHoTT]
equiv_moveL_pM [definition, in MetaCoq.Translations.MiniHoTT]
equiv_moveL_Mp [definition, in MetaCoq.Translations.MiniHoTT]
equiv_moveR_pV [definition, in MetaCoq.Translations.MiniHoTT]
equiv_moveR_Vp [definition, in MetaCoq.Translations.MiniHoTT]
equiv_moveR_pM [definition, in MetaCoq.Translations.MiniHoTT]
equiv_moveR_Mp [definition, in MetaCoq.Translations.MiniHoTT]
equiv_cancelR [definition, in MetaCoq.Translations.MiniHoTT]
equiv_whiskerR [definition, in MetaCoq.Translations.MiniHoTT]
equiv_cancelL [definition, in MetaCoq.Translations.MiniHoTT]
equiv_whiskerL [definition, in MetaCoq.Translations.MiniHoTT]
equiv_concat_lr [definition, in MetaCoq.Translations.MiniHoTT]
equiv_concat_r [definition, in MetaCoq.Translations.MiniHoTT]
equiv_concat_l [definition, in MetaCoq.Translations.MiniHoTT]
equiv_path_inverse [definition, in MetaCoq.Translations.MiniHoTT]
equiv_inj [definition, in MetaCoq.Translations.MiniHoTT]
equiv_ap' [definition, in MetaCoq.Translations.MiniHoTT]
equiv_ap [definition, in MetaCoq.Translations.MiniHoTT]
equiv_composeR' [definition, in MetaCoq.Translations.MiniHoTT]
equiv_ind_comp [definition, in MetaCoq.Translations.MiniHoTT]
equiv_ind [definition, in MetaCoq.Translations.MiniHoTT]
equiv_postcompose' [definition, in MetaCoq.Translations.MiniHoTT]
equiv_postcompose [definition, in MetaCoq.Translations.MiniHoTT]
equiv_precompose' [definition, in MetaCoq.Translations.MiniHoTT]
equiv_precompose [definition, in MetaCoq.Translations.MiniHoTT]
equiv_contr_contr [lemma, in MetaCoq.Translations.MiniHoTT]
equiv_involution [definition, in MetaCoq.Translations.MiniHoTT]
equiv_adjointify [definition, in MetaCoq.Translations.MiniHoTT]
equiv_transport [definition, in MetaCoq.Translations.MiniHoTT]
equiv_inverse [lemma, in MetaCoq.Translations.MiniHoTT]
equiv_homotopic [definition, in MetaCoq.Translations.MiniHoTT]
equiv_compose' [definition, in MetaCoq.Translations.MiniHoTT]
equiv_compose [definition, in MetaCoq.Translations.MiniHoTT]
equiv_idmap [definition, in MetaCoq.Translations.MiniHoTT]
equiv_isequiv [projection, in MetaCoq.Translations.MiniHoTT]
equiv_fun [projection, in MetaCoq.Translations.MiniHoTT]
equiv_inv [projection, in MetaCoq.Translations.MiniHoTT]
equiv_sigma_assoc [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_contr_sigma [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_sigma_contr [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_functor_sigma_id [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_functor_sigma' [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_functor_sigma [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_path_sigma_contra [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_path_sigma [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_flip [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_contr_forall [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_functor_forall_covariant_compose [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_functor_forall_covariant [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_functor_forall_pf [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_functor_forall_pb [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_functor_forall_id [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_functor_forall' [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_functor_forall [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_path_forall [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_apD10 [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_paths_ind [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_moveL_equiv_V [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_moveL_equiv_M [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_moveR_equiv_V [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_moveR_equiv_M [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_moveL_transport_p [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_moveL_transport_V [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_moveR_transport_V [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_moveR_transport_p [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_moveL_pV [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_moveL_Vp [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_moveL_pM [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_moveL_Mp [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_moveR_pV [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_moveR_Vp [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_moveR_pM [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_moveR_Mp [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_cancelR [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_whiskerR [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_cancelL [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_whiskerL [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_concat_lr [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_concat_r [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_concat_l [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_path_inverse [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_inj [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_ap' [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_ap [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_composeR' [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_ind_comp [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_ind [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_postcompose' [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_postcompose [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_precompose' [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_precompose [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_contr_contr [lemma, in MetaCoq.Translations.MiniHoTT_paths]
equiv_involution [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_adjointify [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_transport [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_inverse [lemma, in MetaCoq.Translations.MiniHoTT_paths]
equiv_homotopic [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_compose' [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_compose [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_idmap [definition, in MetaCoq.Translations.MiniHoTT_paths]
equiv_isequiv [projection, in MetaCoq.Translations.MiniHoTT_paths]
equiv_fun [projection, in MetaCoq.Translations.MiniHoTT_paths]
equiv_inv [projection, in MetaCoq.Translations.MiniHoTT_paths]
equiv_contrfib [definition, in MetaCoq.Translations.times_bool_fun2]
equ':248 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
equ':261 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
equ':363 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
equ':73 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
equ:11 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
equ:120 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
equ:149 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
equ:17 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
equ:187 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
equ:20 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
equ:201 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
equ:223 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
equ:247 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
equ:260 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
equ:30 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
equ:333 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
equ:344 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
equ:36 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
equ:362 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
equ:72 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
eq_universe_subset [lemma, in MetaCoq.Template.Universes]
eq_universe_leq_universe' [definition, in MetaCoq.Template.Universes]
eq_universe_equivalence [instance, in MetaCoq.Template.Universes]
eq_levelalg_equivalence [instance, in MetaCoq.Template.Universes]
eq_universe_leq_universe [instance, in MetaCoq.Template.Universes]
eq_leq_universe [lemma, in MetaCoq.Template.Universes]
eq_leq_levelalg [lemma, in MetaCoq.Template.Universes]
eq_universe_trans [instance, in MetaCoq.Template.Universes]
eq_levelalg_trans [instance, in MetaCoq.Template.Universes]
eq_universe_sym [instance, in MetaCoq.Template.Universes]
eq_levelalg_sym [instance, in MetaCoq.Template.Universes]
eq_universe_refl [instance, in MetaCoq.Template.Universes]
eq_levelalg_refl [instance, in MetaCoq.Template.Universes]
eq_universe [definition, in MetaCoq.Template.Universes]
eq_levelalg:526 [binder, in MetaCoq.Template.Universes]
eq_universe_ [definition, in MetaCoq.Template.Universes]
eq_levelalg [definition, in MetaCoq.Template.Universes]
eq_binder_annot [definition, in MetaCoq.Template.BasicAst]
eq_term_eq_termp [lemma, in MetaCoq.PCUIC.PCUICCumulativity]
eq_termp [abbreviation, in MetaCoq.PCUIC.PCUICCumulativity]
eq_termp_napp [definition, in MetaCoq.PCUIC.PCUICCumulativity]
eq_term_mkApps [lemma, in MetaCoq.PCUIC.PCUICCumulativity]
eq_term_eq_term_napp [lemma, in MetaCoq.PCUIC.PCUICCumulativity]
eq_term_App [lemma, in MetaCoq.PCUIC.PCUICCumulativity]
eq_eqáµ— [definition, in MetaCoq.Translations.times_bool_fun]
eq_names_subst_instance_pcuic [lemma, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
eq_names_subst_context_pcuic [lemma, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
eq_binder_trans [lemma, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
eq_names_subst_instance [lemma, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
eq_names_subst_context [lemma, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
eq_names [abbreviation, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
eq_pair_transport [lemma, in MetaCoq.PCUIC.Syntax.PCUICViews]
eq_annots_cstr_branch_context [lemma, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
eq_annots_ind_predicate_context [lemma, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
eq_annots_expand_lets_ctx [lemma, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
eq_binder_annot_eq_context_gen_set_binder_name [lemma, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
eq_context [definition, in MetaCoq.Template.Typing]
eq_decl [definition, in MetaCoq.Template.Typing]
eq_opt_term [definition, in MetaCoq.Template.Typing]
eq_term_nocast [definition, in MetaCoq.Template.Typing]
eq_term_upto_univ_mkApps [lemma, in MetaCoq.Template.TermEquality]
eq_term_App [lemma, in MetaCoq.Template.TermEquality]
eq_term_upto_univ_App [lemma, in MetaCoq.Template.TermEquality]
eq_term_leq_term [lemma, in MetaCoq.Template.TermEquality]
eq_term_upto_univ_impl [instance, in MetaCoq.Template.TermEquality]
eq_term_upto_univ_morphism [lemma, in MetaCoq.Template.TermEquality]
eq_term_upto_univ_morphism0 [lemma, in MetaCoq.Template.TermEquality]
eq_term_refl [lemma, in MetaCoq.Template.TermEquality]
eq_term_upto_univ_refl [lemma, in MetaCoq.Template.TermEquality]
eq_binder_annots_refl [instance, in MetaCoq.Template.TermEquality]
eq_binder_annot_refl [definition, in MetaCoq.Template.TermEquality]
eq_binder_annot_equiv [instance, in MetaCoq.Template.TermEquality]
eq_term [abbreviation, in MetaCoq.Template.TermEquality]
eq_term_upto_univ [abbreviation, in MetaCoq.Template.TermEquality]
eq_Cast [constructor, in MetaCoq.Template.TermEquality]
eq_CoFix [constructor, in MetaCoq.Template.TermEquality]
eq_Fix [constructor, in MetaCoq.Template.TermEquality]
eq_Proj [constructor, in MetaCoq.Template.TermEquality]
eq_Case [constructor, in MetaCoq.Template.TermEquality]
eq_LetIn [constructor, in MetaCoq.Template.TermEquality]
eq_Prod [constructor, in MetaCoq.Template.TermEquality]
eq_Lambda [constructor, in MetaCoq.Template.TermEquality]
eq_Construct [constructor, in MetaCoq.Template.TermEquality]
eq_Ind [constructor, in MetaCoq.Template.TermEquality]
eq_Const [constructor, in MetaCoq.Template.TermEquality]
eq_App [constructor, in MetaCoq.Template.TermEquality]
eq_Sort [constructor, in MetaCoq.Template.TermEquality]
eq_Var [constructor, in MetaCoq.Template.TermEquality]
eq_Evar [constructor, in MetaCoq.Template.TermEquality]
eq_Rel [constructor, in MetaCoq.Template.TermEquality]
eq_term_upto_univ_napp [inductive, in MetaCoq.Template.TermEquality]
eq_term:45 [binder, in MetaCoq.Template.TermEquality]
eq_term_upto_univ_weaken_env [instance, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
eq_term_subset [lemma, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
eq_simpl_pred [definition, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
eq_term_set_binder_name [lemma, in MetaCoq.PCUIC.PCUICValidity]
eq_binder_annots_eq_ctx [lemma, in MetaCoq.PCUIC.PCUICValidity]
eq_context_upto_map2_set_binder_name [lemma, in MetaCoq.PCUIC.PCUICCumulProp]
eq_term_upto_univ_napp_leq [lemma, in MetaCoq.PCUIC.PCUICCumulProp]
eq_term_napp [abbreviation, in MetaCoq.PCUIC.PCUICCumulProp]
eq_term_prop_mkApps_inv [lemma, in MetaCoq.PCUIC.PCUICCumulProp]
eq_term_eq_term_prop_impl [lemma, in MetaCoq.PCUIC.PCUICCumulProp]
eq_term_prop_impl [lemma, in MetaCoq.PCUIC.PCUICCumulProp]
eq_term_prop [definition, in MetaCoq.PCUIC.PCUICCumulProp]
eq_univ_prop [definition, in MetaCoq.PCUIC.PCUICCumulProp]
eq_rect_transport [lemma, in MetaCoq.Template.utils.MCEquality]
eq_annots_inst_case_context [lemma, in MetaCoq.PCUIC.PCUICEquality]
eq_annots_subst_instance_ctx [lemma, in MetaCoq.PCUIC.PCUICEquality]
eq_annots_lift_context [lemma, in MetaCoq.PCUIC.PCUICEquality]
eq_annots_subst_context [lemma, in MetaCoq.PCUIC.PCUICEquality]
eq_annots_fold [lemma, in MetaCoq.PCUIC.PCUICEquality]
eq_context_gen_binder_annot [lemma, in MetaCoq.PCUIC.PCUICEquality]
eq_annots [abbreviation, in MetaCoq.PCUIC.PCUICEquality]
eq_univ_make [lemma, in MetaCoq.PCUIC.PCUICEquality]
eq_term_upto_univ_napp_flip [lemma, in MetaCoq.PCUIC.PCUICEquality]
eq_term_upto_univ_mkApps_inv [lemma, in MetaCoq.PCUIC.PCUICEquality]
eq_term_it_mkLambda_or_LetIn_inv [lemma, in MetaCoq.PCUIC.PCUICEquality]
eq_term_it_mkProd_or_LetIn [lemma, in MetaCoq.PCUIC.PCUICEquality]
eq_term_upto_univ_it_mkProd_or_LetIn [lemma, in MetaCoq.PCUIC.PCUICEquality]
eq_term_it_mkLambda_or_LetIn [lemma, in MetaCoq.PCUIC.PCUICEquality]
eq_term_upto_univ_it_mkLambda_or_LetIn_r [lemma, in MetaCoq.PCUIC.PCUICEquality]
eq_term_upto_univ_it_mkLambda_or_LetIn [lemma, in MetaCoq.PCUIC.PCUICEquality]
eq_context_impl [lemma, in MetaCoq.PCUIC.PCUICEquality]
eq_context_upto_nth_error [lemma, in MetaCoq.PCUIC.PCUICEquality]
eq_context_upto_smash_context [lemma, in MetaCoq.PCUIC.PCUICEquality]
eq_context_upto_subst_context [lemma, in MetaCoq.PCUIC.PCUICEquality]
eq_context_upto_length [lemma, in MetaCoq.PCUIC.PCUICEquality]
eq_context_upto_rev' [lemma, in MetaCoq.PCUIC.PCUICEquality]
eq_context_upto_rev [lemma, in MetaCoq.PCUIC.PCUICEquality]
eq_context_upto_cat [lemma, in MetaCoq.PCUIC.PCUICEquality]
eq_context_upto_sym [lemma, in MetaCoq.PCUIC.PCUICEquality]
eq_context_upto_refl [lemma, in MetaCoq.PCUIC.PCUICEquality]
eq_decl_upto_gen [definition, in MetaCoq.PCUIC.PCUICEquality]
eq_term_upto_univ_isApp [lemma, in MetaCoq.PCUIC.PCUICEquality]
eq_term_upto_univ_mkApps_r_inv [lemma, in MetaCoq.PCUIC.PCUICEquality]
eq_term_upto_univ_mkApps_l_inv [lemma, in MetaCoq.PCUIC.PCUICEquality]
eq_term_upto_univ_mkApps [lemma, in MetaCoq.PCUIC.PCUICEquality]
eq_term_upto_univ_napp_mkApps_r_inv [lemma, in MetaCoq.PCUIC.PCUICEquality]
eq_term_upto_univ_napp_mkApps_l_inv [lemma, in MetaCoq.PCUIC.PCUICEquality]
eq_term_upto_univ_napp_mkApps [lemma, in MetaCoq.PCUIC.PCUICEquality]
eq_term_eq_term_napp [lemma, in MetaCoq.PCUIC.PCUICEquality]
eq_term_upto_univ_subst [lemma, in MetaCoq.PCUIC.PCUICEquality]
eq_term_upto_univ_substs [lemma, in MetaCoq.PCUIC.PCUICEquality]
eq_term_upto_univ_lift [lemma, in MetaCoq.PCUIC.PCUICEquality]
eq_term_leq_term [instance, in MetaCoq.PCUIC.PCUICEquality]
eq_term_upto_univ_leq [instance, in MetaCoq.PCUIC.PCUICEquality]
eq_term_upto_univ_empty_impl [instance, in MetaCoq.PCUIC.PCUICEquality]
eq_term_upto_univ_impl [instance, in MetaCoq.PCUIC.PCUICEquality]
eq_term':365 [binder, in MetaCoq.PCUIC.PCUICEquality]
eq_term:364 [binder, in MetaCoq.PCUIC.PCUICEquality]
eq_term_upto_univ_antisym [lemma, in MetaCoq.PCUIC.PCUICEquality]
eq_term_equiv [instance, in MetaCoq.PCUIC.PCUICEquality]
eq_context_equiv [instance, in MetaCoq.PCUIC.PCUICEquality]
eq_term_upto_univ_equiv [instance, in MetaCoq.PCUIC.PCUICEquality]
eq_term_upto_univ_trans [instance, in MetaCoq.PCUIC.PCUICEquality]
eq_predicate_trans [instance, in MetaCoq.PCUIC.PCUICEquality]
eq_term:278 [binder, in MetaCoq.PCUIC.PCUICEquality]
eq_predicate_sym [instance, in MetaCoq.PCUIC.PCUICEquality]
eq_term_upto_univ_sym [instance, in MetaCoq.PCUIC.PCUICEquality]
eq_term:257 [binder, in MetaCoq.PCUIC.PCUICEquality]
eq_term_upto_univ_refl [instance, in MetaCoq.PCUIC.PCUICEquality]
eq_predicate_refl [instance, in MetaCoq.PCUIC.PCUICEquality]
eq_term:234 [binder, in MetaCoq.PCUIC.PCUICEquality]
eq_binder_relevances_refl [lemma, in MetaCoq.PCUIC.PCUICEquality]
eq_binder_annot_refl [definition, in MetaCoq.PCUIC.PCUICEquality]
eq_binder_annot_equiv [instance, in MetaCoq.PCUIC.PCUICEquality]
eq_context_upto [abbreviation, in MetaCoq.PCUIC.PCUICEquality]
eq_context [abbreviation, in MetaCoq.PCUIC.PCUICEquality]
eq_decl [abbreviation, in MetaCoq.PCUIC.PCUICEquality]
eq_term [abbreviation, in MetaCoq.PCUIC.PCUICEquality]
eq_term_upto_univ [abbreviation, in MetaCoq.PCUIC.PCUICEquality]
eq_CoFix [constructor, in MetaCoq.PCUIC.PCUICEquality]
eq_Fix [constructor, in MetaCoq.PCUIC.PCUICEquality]
eq_Proj [constructor, in MetaCoq.PCUIC.PCUICEquality]
eq_Case [constructor, in MetaCoq.PCUIC.PCUICEquality]
eq_LetIn [constructor, in MetaCoq.PCUIC.PCUICEquality]
eq_Prod [constructor, in MetaCoq.PCUIC.PCUICEquality]
eq_Lambda [constructor, in MetaCoq.PCUIC.PCUICEquality]
eq_Construct [constructor, in MetaCoq.PCUIC.PCUICEquality]
eq_Ind [constructor, in MetaCoq.PCUIC.PCUICEquality]
eq_Const [constructor, in MetaCoq.PCUIC.PCUICEquality]
eq_App [constructor, in MetaCoq.PCUIC.PCUICEquality]
eq_Sort [constructor, in MetaCoq.PCUIC.PCUICEquality]
eq_Var [constructor, in MetaCoq.PCUIC.PCUICEquality]
eq_Evar [constructor, in MetaCoq.PCUIC.PCUICEquality]
eq_Rel [constructor, in MetaCoq.PCUIC.PCUICEquality]
eq_term_upto_univ_napp [inductive, in MetaCoq.PCUIC.PCUICEquality]
eq_term:111 [binder, in MetaCoq.PCUIC.PCUICEquality]
eq_predicate [definition, in MetaCoq.PCUIC.PCUICEquality]
eq_term:109 [binder, in MetaCoq.PCUIC.PCUICEquality]
eq_context_trans [instance, in MetaCoq.PCUIC.PCUICEquality]
eq_term:107 [binder, in MetaCoq.PCUIC.PCUICEquality]
eq_context_sym [instance, in MetaCoq.PCUIC.PCUICEquality]
eq_term:105 [binder, in MetaCoq.PCUIC.PCUICEquality]
eq_context_refl [instance, in MetaCoq.PCUIC.PCUICEquality]
eq_term:103 [binder, in MetaCoq.PCUIC.PCUICEquality]
eq_term:101 [binder, in MetaCoq.PCUIC.PCUICEquality]
eq_term:99 [binder, in MetaCoq.PCUIC.PCUICEquality]
eq_term:93 [binder, in MetaCoq.PCUIC.PCUICEquality]
eq_term:83 [binder, in MetaCoq.PCUIC.PCUICEquality]
eq_term':75 [binder, in MetaCoq.PCUIC.PCUICEquality]
eq_term:73 [binder, in MetaCoq.PCUIC.PCUICEquality]
eq_term':70 [binder, in MetaCoq.PCUIC.PCUICEquality]
eq_term:68 [binder, in MetaCoq.PCUIC.PCUICEquality]
eq_context_gen_impl [lemma, in MetaCoq.PCUIC.PCUICEquality]
eq_term':66 [binder, in MetaCoq.PCUIC.PCUICEquality]
eq_term:64 [binder, in MetaCoq.PCUIC.PCUICEquality]
eq_context_upto_names_gen [lemma, in MetaCoq.PCUIC.PCUICEquality]
eq_context_gen [abbreviation, in MetaCoq.PCUIC.PCUICEquality]
eq_context_upto_names [abbreviation, in MetaCoq.PCUIC.PCUICEquality]
eq_term:48 [binder, in MetaCoq.PCUIC.PCUICEquality]
eq_projection_refl [lemma, in MetaCoq.Template.Kernames]
eq_projection [definition, in MetaCoq.Template.Kernames]
eq_inductive_refl [lemma, in MetaCoq.Template.Kernames]
eq_inductive [abbreviation, in MetaCoq.Template.Kernames]
eq_inductive_def [definition, in MetaCoq.Template.Kernames]
eq_constant [definition, in MetaCoq.Template.Kernames]
eq_kername_refl [lemma, in MetaCoq.Template.Kernames]
eq_kername [abbreviation, in MetaCoq.Template.Kernames]
eq_term_valid_pos [lemma, in MetaCoq.PCUIC.Syntax.PCUICPosition]
eq_term_upto_valid_pos [lemma, in MetaCoq.PCUIC.Syntax.PCUICPosition]
eq_context_upto_context_choice_term [lemma, in MetaCoq.PCUIC.Syntax.PCUICPosition]
eq_npars:118 [binder, in MetaCoq.PCUIC.PCUICInversion]
eq_term_upto_univ_napp_0 [lemma, in MetaCoq.PCUIC.PCUICAlpha]
eq_context_conversion [lemma, in MetaCoq.PCUIC.PCUICAlpha]
eq_binder_annots_eq_context_gen_ctx [lemma, in MetaCoq.PCUIC.PCUICAlpha]
eq_context_gen_upto [lemma, in MetaCoq.PCUIC.PCUICAlpha]
eq_context_upto_subst_instance [lemma, in MetaCoq.PCUIC.PCUICAlpha]
eq_context_upto_lift_context [lemma, in MetaCoq.PCUIC.PCUICAlpha]
eq_context_upto_map2_set_binder_name [lemma, in MetaCoq.PCUIC.PCUICAlpha]
eq_context_upto_conv_context_rel [lemma, in MetaCoq.PCUIC.PCUICAlpha]
eq_context_upto_empty_impl [lemma, in MetaCoq.PCUIC.PCUICAlpha]
eq_prod_refl [lemma, in MetaCoq.Template.utils.ReflectEq]
eq_prod [definition, in MetaCoq.Template.utils.ReflectEq]
eq_sig_true [definition, in MetaCoq.Template.utils.ReflectEq]
eq_bool [definition, in MetaCoq.Template.utils.ReflectEq]
eq_list [section, in MetaCoq.Template.utils.ReflectEq]
eq_option [definition, in MetaCoq.Template.utils.ReflectEq]
eq_dec_to_bool [definition, in MetaCoq.Template.utils.ReflectEq]
eq_annots_expand_lets_ctx [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
eq_names_subst_instance_pcuic [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
eq_names_subst_context_pcuic [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
eq_term_upto_univ_expand_lets [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
eq_context_upto_context_assumptions [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
eq_context_gen_smash_context [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
eq_context_gen_extended_subst [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
eq_binder_trans [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
eq_names_smash_context [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
eq_max [definition, in MetaCoq.Template.utils.wGraph]
eq_termp_mkApps_inv [lemma, in MetaCoq.PCUIC.PCUICConvCumInversion]
eq_term_upto_univ_napp_nonind [lemma, in MetaCoq.PCUIC.PCUICConvCumInversion]
eq_term_eq_termp [lemma, in MetaCoq.PCUIC.PCUICConvCumInversion]
eq_term_upto_univ_inst [lemma, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
eq_term [abbreviation, in MetaCoq.SafeChecker.PCUICSafeConversion]
eq_term_valid_pos [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
eq_term [definition, in MetaCoq.Template.Checker]
eq_case_info [definition, in MetaCoq.Template.Checker]
eq_context_upto_inst_case_context [lemma, in MetaCoq.PCUIC.PCUICPrincipality]
eq_term_upto_univ_napp_leq [lemma, in MetaCoq.PCUIC.PCUICPrincipality]
eq_term_napp [abbreviation, in MetaCoq.PCUIC.PCUICPrincipality]
eq_context_empty_eq_context [lemma, in MetaCoq.PCUIC.PCUICPrincipality]
eq_term_empty_eq_term [lemma, in MetaCoq.PCUIC.PCUICPrincipality]
eq_term_empty_leq_term [lemma, in MetaCoq.PCUIC.PCUICPrincipality]
eq_term_leq_term [lemma, in MetaCoq.PCUIC.PCUICPrincipality]
eq_form [lemma, in MetaCoq.Examples.tauto]
eq_var [lemma, in MetaCoq.Examples.tauto]
eq_decl_reflect [instance, in MetaCoq.Template.Reflect]
eq_cast_kind [definition, in MetaCoq.Template.Reflect]
eq_def [definition, in MetaCoq.Template.Reflect]
eq_aname [definition, in MetaCoq.Template.Reflect]
eq_relevance [definition, in MetaCoq.Template.Reflect]
eq_name [definition, in MetaCoq.Template.Reflect]
eq_levels [definition, in MetaCoq.Template.Reflect]
eq_prop_level [definition, in MetaCoq.Template.Reflect]
eq_predicate [instance, in MetaCoq.Template.ReflectAst]
eq_term_nl_eq [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
eq_context_nl [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
eq_context_nl_IH [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
eq_context_gen_upto [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
eq_term_upto_univ_napp_on_free_vars [lemma, in MetaCoq.PCUIC.PCUICConfluence]
eq_context_upto_names_red_ctx_alpha [lemma, in MetaCoq.PCUIC.PCUICConfluence]
eq_context_upto_names_red_ctx [lemma, in MetaCoq.PCUIC.PCUICConfluence]
eq_context_upto_names_app [lemma, in MetaCoq.PCUIC.PCUICConfluence]
eq_context_upto_names_on_free_vars [lemma, in MetaCoq.PCUIC.PCUICConfluence]
eq_context_upto_flip [lemma, in MetaCoq.PCUIC.PCUICConfluence]
eq_context_upto_univ_subst_instance' [lemma, in MetaCoq.PCUIC.PCUICConfluence]
eq_context_upto_univ_subst_instance [lemma, in MetaCoq.PCUIC.PCUICConfluence]
eq_term_upto_univ_subst_instance' [lemma, in MetaCoq.PCUIC.PCUICConfluence]
eq_context_gen_eq_univ_subst_preserved [lemma, in MetaCoq.PCUIC.PCUICConfluence]
eq_context_upto_univ_subst_preserved [instance, in MetaCoq.PCUIC.PCUICConfluence]
eq_context_gen_eq_context_upto [lemma, in MetaCoq.PCUIC.PCUICConfluence]
eq_context_extended_subst [lemma, in MetaCoq.PCUIC.PCUICConfluence]
eq_context_gen_context_assumptions [lemma, in MetaCoq.PCUIC.PCUICConfluence]
eq_one_decl [abbreviation, in MetaCoq.PCUIC.PCUICConfluence]
eq_ctx [instance, in MetaCoq.PCUIC.Syntax.PCUICReflect]
eq_term_inds [lemma, in MetaCoq.PCUIC.PCUICConversion]
eq_term_compare_term [lemma, in MetaCoq.PCUIC.PCUICConversion]
eq_context_upto_ws_cumul_ctx_pb [lemma, in MetaCoq.PCUIC.PCUICConversion]
eq_term_fix_or_cofix [lemma, in MetaCoq.PCUIC.PCUICConversion]
eq_context_gen_inst_case_context [lemma, in MetaCoq.PCUIC.PCUICConversion]
eq_context_gen_subst_context [lemma, in MetaCoq.PCUIC.PCUICConversion]
eq_term_upto_univ_conv_arity_r [lemma, in MetaCoq.PCUIC.PCUICConversion]
eq_term_upto_univ_conv_arity_l [lemma, in MetaCoq.PCUIC.PCUICConversion]
eq_terms_ws_cumul_pb_terms [lemma, in MetaCoq.PCUIC.PCUICConversion]
eq_term_upto_univ_cumulSpec [lemma, in MetaCoq.PCUIC.PCUICConversion]
eq_term_upto_univ_napp_cumulSpec [lemma, in MetaCoq.PCUIC.PCUICConversion]
eq_npars:53 [binder, in MetaCoq.PCUIC.PCUICTyping]
eq_binder_annots_eq [lemma, in MetaCoq.PCUIC.PCUICCasesContexts]
eq_names_subst_instance [lemma, in MetaCoq.PCUIC.PCUICCasesContexts]
eq_names_subst_context [lemma, in MetaCoq.PCUIC.PCUICCasesContexts]
eq_names [abbreviation, in MetaCoq.PCUIC.PCUICCasesContexts]
eq_context_upto_univ_cumul_context [lemma, in MetaCoq.PCUIC.PCUICContextConversion]
eq_context_upto_univ_conv_context [lemma, in MetaCoq.PCUIC.PCUICContextConversion]
eq_context_upto_empty_conv_context [lemma, in MetaCoq.PCUIC.PCUICContextConversion]
eq_subrel_eq_univ [instance, in MetaCoq.PCUIC.PCUICContextConversion]
eq_context_upto_cumul_context [lemma, in MetaCoq.PCUIC.PCUICContextConversion]
eq_context_upto_conv_context [lemma, in MetaCoq.PCUIC.PCUICContextConversion]
eq_leq_context_upto [lemma, in MetaCoq.PCUIC.PCUICContextConversion]
eq_context_upto_impl [lemma, in MetaCoq.PCUIC.PCUICContextConversion]
eq_context_upto_names_upto_names [lemma, in MetaCoq.PCUIC.PCUICSR]
eq_ws_cumul_pb_terms_trans [lemma, in MetaCoq.PCUIC.PCUICSR]
eq_ws_cumul_pb_trans [lemma, in MetaCoq.PCUIC.PCUICSR]
eq_context_alpha_to_extended_list [lemma, in MetaCoq.PCUIC.PCUICSR]
eq_context_alpha_reln [lemma, in MetaCoq.PCUIC.PCUICSR]
eq_context_alpha_conv [lemma, in MetaCoq.PCUIC.PCUICSR]
eq_term_subst_instance [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
eq_term_upto_univ_subst_preserved [instance, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
eq_universe_subst_instance [instance, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
eq_universe_SubstUnivPreserving [instance, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
eq_term_upto_univ_subst_instance [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
eq_valuation [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
eq_term_upto_univ_rename [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
eq_context_upto_univ_cumul_context [lemma, in MetaCoq.SafeChecker.PCUICSafeChecker]
eq_context_upto_cumul_context [lemma, in MetaCoq.SafeChecker.PCUICSafeChecker]
eq_decl_upto_refl [lemma, in MetaCoq.SafeChecker.PCUICSafeChecker]
eq_decl_eq_decl_upto [lemma, in MetaCoq.SafeChecker.PCUICSafeChecker]
eq_tip_skipn [lemma, in MetaCoq.Template.TypingWf]
eq_decompose_app [lemma, in MetaCoq.Template.TypingWf]
eq_names_subst_instance [lemma, in MetaCoq.PCUIC.PCUICContexts]
eq_names_subst_context [lemma, in MetaCoq.PCUIC.PCUICContexts]
eq_names [abbreviation, in MetaCoq.PCUIC.PCUICContexts]
eq_context_alpha_conv [lemma, in MetaCoq.PCUIC.PCUICSpine]
eq_term [abbreviation, in MetaCoq.SafeChecker.PCUICEqualityDec]
eq_universeP [lemma, in MetaCoq.SafeChecker.PCUICEqualityDec]
eq_term_upto_univ_refl_wf [definition, in MetaCoq.SafeChecker.PCUICEqualityDec]
eq_dec_to_bool_refl [lemma, in MetaCoq.SafeChecker.PCUICEqualityDec]
eq_params:1088 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
eq_context_gen_wf_branch [lemma, in MetaCoq.SafeChecker.PCUICTypeChecker]
eq_context_gen_wf_predicate [lemma, in MetaCoq.SafeChecker.PCUICTypeChecker]
eq':39 [binder, in MetaCoq.Examples.add_constructor]
eq':841 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
eq0_leq0_levelalg [lemma, in MetaCoq.Template.Universes]
eq0_levelalg [definition, in MetaCoq.Template.Universes]
eq1:2164 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
eq2:2165 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
eq:1018 [binder, in MetaCoq.PCUIC.PCUICTyping]
eq:1072 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
eq:1073 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
eq:1124 [binder, in MetaCoq.PCUIC.PCUICConfluence]
eq:1128 [binder, in MetaCoq.PCUIC.PCUICConfluence]
eq:1132 [binder, in MetaCoq.PCUIC.PCUICConfluence]
eq:1235 [binder, in MetaCoq.PCUIC.PCUICConfluence]
eq:1306 [binder, in MetaCoq.Template.Typing]
eq:1329 [binder, in MetaCoq.Template.Typing]
eq:187 [binder, in MetaCoq.Template.utils.wGraph]
eq:24 [binder, in MetaCoq.PCUIC.Syntax.PCUICViews]
eq:259 [binder, in MetaCoq.Template.common.uGraph]
eq:282 [binder, in MetaCoq.PCUIC.PCUICConfluence]
eq:381 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
eq:54 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
eq:58 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
eq:636 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
eq:840 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
eq:924 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
eq:957 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
eq:984 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
eq:997 [binder, in MetaCoq.PCUIC.PCUICTyping]
eqΓ0:571 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
eqΓ0:581 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
eqáµ—_unit_unit [lemma, in MetaCoq.Translations.times_bool_fun]
eqáµ—_eq [definition, in MetaCoq.Translations.times_bool_fun]
erasable_tBox_value [lemma, in MetaCoq.Erasure.ErasureFunction]
erase [definition, in MetaCoq.Erasure.ErasureFunction]
Erase [section, in MetaCoq.Erasure.ErasureFunction]
EraseGlobalFast [section, in MetaCoq.Erasure.ErasureFunction]
erases [inductive, in MetaCoq.Erasure.Extract]
erases_subst0 [lemma, in MetaCoq.Erasure.ESubstitution]
erases_subst [lemma, in MetaCoq.Erasure.ESubstitution]
erases_eq [lemma, in MetaCoq.Erasure.ESubstitution]
erases_weakening [lemma, in MetaCoq.Erasure.ESubstitution]
erases_weakening' [lemma, in MetaCoq.Erasure.ESubstitution]
erases_ctx_ext [lemma, in MetaCoq.Erasure.ESubstitution]
erases_extends [lemma, in MetaCoq.Erasure.ESubstitution]
erases_global_wf_glob [lemma, in MetaCoq.Erasure.ErasureCorrectness]
erases_mutual_inductive_body_wf [lemma, in MetaCoq.Erasure.ErasureCorrectness]
erases_global_decls_fresh [lemma, in MetaCoq.Erasure.ErasureCorrectness]
erases_global_closed_env [lemma, in MetaCoq.Erasure.ErasureCorrectness]
erases_correct [lemma, in MetaCoq.Erasure.ErasureCorrectness]
erases_global_erases_deps [lemma, in MetaCoq.Erasure.EDeps]
erases_global_all_deps [lemma, in MetaCoq.Erasure.EDeps]
erases_deps_single [lemma, in MetaCoq.Erasure.EDeps]
erases_declared_constructor [lemma, in MetaCoq.Erasure.EDeps]
erases_deps_cons [lemma, in MetaCoq.Erasure.EDeps]
erases_deps_forall_ind [lemma, in MetaCoq.Erasure.EDeps]
erases_deps_eval [lemma, in MetaCoq.Erasure.EDeps]
erases_deps_cunfold_cofix [lemma, in MetaCoq.Erasure.EDeps]
erases_deps_cunfold_fix [lemma, in MetaCoq.Erasure.EDeps]
erases_deps_substl [lemma, in MetaCoq.Erasure.EDeps]
erases_deps_csubst [lemma, in MetaCoq.Erasure.EDeps]
erases_deps_subst1 [lemma, in MetaCoq.Erasure.EDeps]
erases_deps_subst [lemma, in MetaCoq.Erasure.EDeps]
erases_deps_lift [lemma, in MetaCoq.Erasure.EDeps]
erases_deps_mkApps_inv [lemma, in MetaCoq.Erasure.EDeps]
erases_deps_mkApps [lemma, in MetaCoq.Erasure.EDeps]
erases_deps_tCoFix [constructor, in MetaCoq.Erasure.Extract]
erases_deps_tFix [constructor, in MetaCoq.Erasure.Extract]
erases_deps_tProj [constructor, in MetaCoq.Erasure.Extract]
erases_deps_tCase [constructor, in MetaCoq.Erasure.Extract]
erases_deps_tConstruct [constructor, in MetaCoq.Erasure.Extract]
erases_deps_tConst [constructor, in MetaCoq.Erasure.Extract]
erases_deps_tApp [constructor, in MetaCoq.Erasure.Extract]
erases_deps_tLetIn [constructor, in MetaCoq.Erasure.Extract]
erases_deps_tLambda [constructor, in MetaCoq.Erasure.Extract]
erases_deps_tEvar [constructor, in MetaCoq.Erasure.Extract]
erases_deps_tVar [constructor, in MetaCoq.Erasure.Extract]
erases_deps_tRel [constructor, in MetaCoq.Erasure.Extract]
erases_deps_tBox [constructor, in MetaCoq.Erasure.Extract]
erases_deps [inductive, in MetaCoq.Erasure.Extract]
erases_global [definition, in MetaCoq.Erasure.Extract]
erases_global_ind [constructor, in MetaCoq.Erasure.Extract]
erases_global_cnst [constructor, in MetaCoq.Erasure.Extract]
erases_global_nil [constructor, in MetaCoq.Erasure.Extract]
erases_global_decls [inductive, in MetaCoq.Erasure.Extract]
erases_mutual_inductive_body [definition, in MetaCoq.Erasure.Extract]
erases_one_inductive_body [definition, in MetaCoq.Erasure.Extract]
erases_constant_body [definition, in MetaCoq.Erasure.Extract]
erases_forall_list_ind [lemma, in MetaCoq.Erasure.Extract]
erases_box [constructor, in MetaCoq.Erasure.Extract]
erases_tCoFix [constructor, in MetaCoq.Erasure.Extract]
erases_tFix [constructor, in MetaCoq.Erasure.Extract]
erases_tProj [constructor, in MetaCoq.Erasure.Extract]
erases_tCase1 [constructor, in MetaCoq.Erasure.Extract]
erases_tConstruct [constructor, in MetaCoq.Erasure.Extract]
erases_tConst [constructor, in MetaCoq.Erasure.Extract]
erases_tApp [constructor, in MetaCoq.Erasure.Extract]
erases_tLetIn [constructor, in MetaCoq.Erasure.Extract]
erases_tLambda [constructor, in MetaCoq.Erasure.Extract]
erases_tEvar [constructor, in MetaCoq.Erasure.Extract]
erases_tVar [constructor, in MetaCoq.Erasure.Extract]
erases_tRel [constructor, in MetaCoq.Erasure.Extract]
erases_wellformed [lemma, in MetaCoq.Erasure.ErasureProperties]
erases_closed [lemma, in MetaCoq.Erasure.ErasureProperties]
erases_subst_instance_decl [lemma, in MetaCoq.Erasure.ErasureProperties]
erases_subst_instance'' [lemma, in MetaCoq.Erasure.ErasureProperties]
erases_subst_instance [lemma, in MetaCoq.Erasure.ErasureProperties]
erases_subst_instance0 [lemma, in MetaCoq.Erasure.ErasureProperties]
erases_context_conversion [lemma, in MetaCoq.Erasure.ErasureProperties]
erases_isLambda [lemma, in MetaCoq.Erasure.ErasureProperties]
erases_mkApps_inv [lemma, in MetaCoq.Erasure.ErasureProperties]
erases_mkApps [lemma, in MetaCoq.Erasure.ErasureProperties]
erases_App [lemma, in MetaCoq.Erasure.ErasureProperties]
erases_ext_eq [lemma, in MetaCoq.Erasure.ErasureProperties]
erases_wf_fixpoints [lemma, in MetaCoq.Erasure.ErasureFunction]
erases_deps_wellformed [lemma, in MetaCoq.Erasure.ErasureFunction]
erases_deps_erase_weaken [lemma, in MetaCoq.Erasure.ErasureFunction]
erases_deps_erase [lemma, in MetaCoq.Erasure.ErasureFunction]
erases_mutual [lemma, in MetaCoq.Erasure.ErasureFunction]
erases_deps_weaken [lemma, in MetaCoq.Erasure.ErasureFunction]
erases_weakeninv_env [lemma, in MetaCoq.Erasure.ErasureFunction]
erases_erase [lemma, in MetaCoq.Erasure.ErasureFunction]
erase_context [definition, in MetaCoq.Erasure.Extract]
erase_wellformed_fast [lemma, in MetaCoq.Erasure.ErasureFunction]
erase_global_fast_wf_glob [lemma, in MetaCoq.Erasure.ErasureFunction]
erase_global_fast [definition, in MetaCoq.Erasure.ErasureFunction]
erase_global_deps_fast_spec [lemma, in MetaCoq.Erasure.ErasureFunction]
erase_global_deps_fast_spec_gen [lemma, in MetaCoq.Erasure.ErasureFunction]
erase_global_decls_fast [definition, in MetaCoq.Erasure.ErasureFunction]
erase_correct_strong [lemma, in MetaCoq.Erasure.ErasureFunction]
erase_correct_strong' [lemma, in MetaCoq.Erasure.ErasureFunction]
erase_eval_to_box_eager [lemma, in MetaCoq.Erasure.ErasureFunction]
erase_eval_to_box [lemma, in MetaCoq.Erasure.ErasureFunction]
erase_global_decls_wf_glob [lemma, in MetaCoq.Erasure.ErasureFunction]
erase_global_ind_decl_wf_glob [lemma, in MetaCoq.Erasure.ErasureFunction]
erase_global_cst_decl_wf_glob [lemma, in MetaCoq.Erasure.ErasureFunction]
erase_constant_body_correct'' [lemma, in MetaCoq.Erasure.ErasureFunction]
erase_wellformed_weaken [lemma, in MetaCoq.Erasure.ErasureFunction]
erase_wellformed [lemma, in MetaCoq.Erasure.ErasureFunction]
erase_wf_fixpoints [lemma, in MetaCoq.Erasure.ErasureFunction]
erase_global_closed [lemma, in MetaCoq.Erasure.ErasureFunction]
erase_cofix_eq [lemma, in MetaCoq.Erasure.ErasureFunction]
erase_fix_eq [lemma, in MetaCoq.Erasure.ErasureFunction]
erase_brs_eq [lemma, in MetaCoq.Erasure.ErasureFunction]
erase_global_decls_fresh [lemma, in MetaCoq.Erasure.ErasureFunction]
erase_global_declared_constructor [lemma, in MetaCoq.Erasure.ErasureFunction]
erase_mkApps [lemma, in MetaCoq.Erasure.ErasureFunction]
erase_correct [lemma, in MetaCoq.Erasure.ErasureFunction]
erase_global_includes [lemma, in MetaCoq.Erasure.ErasureFunction]
erase_constant_body_correct' [lemma, in MetaCoq.Erasure.ErasureFunction]
erase_constant_body_correct [lemma, in MetaCoq.Erasure.ErasureFunction]
erase_global_erases_deps [lemma, in MetaCoq.Erasure.ErasureFunction]
erase_global_decls_irr [lemma, in MetaCoq.Erasure.ErasureFunction]
erase_global_decls [definition, in MetaCoq.Erasure.ErasureFunction]
erase_constant_body_suffix [lemma, in MetaCoq.Erasure.ErasureFunction]
erase_irrel_global_env [lemma, in MetaCoq.Erasure.ErasureFunction]
erase_mutual_inductive_body [definition, in MetaCoq.Erasure.ErasureFunction]
erase_one_inductive_body [definition, in MetaCoq.Erasure.ErasureFunction]
erase_constant_body [definition, in MetaCoq.Erasure.ErasureFunction]
erase_to_box [lemma, in MetaCoq.Erasure.ErasureFunction]
erase_terms_eq [lemma, in MetaCoq.Erasure.ErasureFunction]
erase_irrel [lemma, in MetaCoq.Erasure.ErasureFunction]
erase_cofix [definition, in MetaCoq.Erasure.ErasureFunction]
erase_fix [definition, in MetaCoq.Erasure.ErasureFunction]
erase_brs [definition, in MetaCoq.Erasure.ErasureFunction]
erase_terms [definition, in MetaCoq.Erasure.ErasureFunction]
erase_prim [definition, in MetaCoq.Erasure.ErasureFunction]
erase_transform [definition, in MetaCoq.Erasure.ETransform]
erase_program [definition, in MetaCoq.Erasure.ETransform]
erase_pcuic_program [definition, in MetaCoq.Erasure.ETransform]
erase_fast_and_print_template_program [definition, in MetaCoq.Erasure.Erasure]
erase_and_print_template_program [definition, in MetaCoq.Erasure.Erasure]
Erasure [library]
ErasureCorrectness [library]
ErasureFunction [library]
ErasureProperties [library]
erasure_pipeline_fast [definition, in MetaCoq.Erasure.Erasure]
erasure_pipeline [definition, in MetaCoq.Erasure.Erasure]
EReflect [library]
ERemoveParams [library]
Error [constructor, in MetaCoq.Translations.translation_utils]
Error [constructor, in MetaCoq.SafeChecker.PCUICSafeConversion]
ESpineView [library]
ESubstitution [library]
es:267 [binder, in MetaCoq.Template.Universes]
es:283 [binder, in MetaCoq.Template.Universes]
es:777 [binder, in MetaCoq.Template.utils.wGraph]
es:779 [binder, in MetaCoq.Template.utils.wGraph]
es:782 [binder, in MetaCoq.Template.utils.wGraph]
Eta [section, in MetaCoq.Template.EtaExpand]
EtaExpand [library]
etaExp_fixsubst [lemma, in MetaCoq.Erasure.EEtaExpandedFix]
etaExp_csubst [lemma, in MetaCoq.Erasure.EEtaExpandedFix]
etaExp_csubst' [lemma, in MetaCoq.Erasure.EEtaExpandedFix]
etaExp_csubst [lemma, in MetaCoq.Erasure.EEtaExpanded]
eta_expand_global_env_expanded [lemma, in MetaCoq.Template.EtaExpand]
eta_expand_global_decl_expanded [lemma, in MetaCoq.Template.EtaExpand]
eta_context_length [lemma, in MetaCoq.Template.EtaExpand]
eta_expand_context_sorts [lemma, in MetaCoq.Template.EtaExpand]
eta_expand_context [lemma, in MetaCoq.Template.EtaExpand]
eta_declared_constructor [lemma, in MetaCoq.Template.EtaExpand]
eta_lookup_global_error [lemma, in MetaCoq.Template.EtaExpand]
eta_lookup_global [lemma, in MetaCoq.Template.EtaExpand]
eta_expand_expanded [lemma, in MetaCoq.Template.EtaExpand]
eta_expand_program [definition, in MetaCoq.Template.EtaExpand]
eta_expand_global_env [definition, in MetaCoq.Template.EtaExpand]
eta_global_declarations [definition, in MetaCoq.Template.EtaExpand]
eta_global_declaration [definition, in MetaCoq.Template.EtaExpand]
eta_minductive_decl [definition, in MetaCoq.Template.EtaExpand]
eta_inductive_decl [definition, in MetaCoq.Template.EtaExpand]
eta_constructor_decl [definition, in MetaCoq.Template.EtaExpand]
eta_context [definition, in MetaCoq.Template.EtaExpand]
eta_global_decl [definition, in MetaCoq.Template.EtaExpand]
eta_expand [definition, in MetaCoq.Template.EtaExpand]
eta_fixpoint [definition, in MetaCoq.Template.EtaExpand]
eta_constructor [definition, in MetaCoq.Template.EtaExpand]
eta_args:8 [binder, in MetaCoq.Template.EtaExpand]
eta_single [definition, in MetaCoq.Template.EtaExpand]
eta_expand [definition, in MetaCoq.Template.TemplateCheckWf]
eta_global_env [lemma, in MetaCoq.Erasure.ErasureFunction]
eta_expand_erase [lemma, in MetaCoq.Erasure.ErasureFunction]
eta_pair [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
eta_path_sigma [definition, in MetaCoq.Translations.MiniHoTT]
eta_path_sigma_uncurried [definition, in MetaCoq.Translations.MiniHoTT]
eta_sigma [definition, in MetaCoq.Translations.MiniHoTT]
eta_path_forall [definition, in MetaCoq.Translations.MiniHoTT]
eta_path_sigma [definition, in MetaCoq.Translations.MiniHoTT_paths]
eta_path_sigma_uncurried [definition, in MetaCoq.Translations.MiniHoTT_paths]
eta_sigma [definition, in MetaCoq.Translations.MiniHoTT_paths]
eta_path_forall [definition, in MetaCoq.Translations.MiniHoTT_paths]
eta_template_global_env [lemma, in MetaCoq.PCUIC.TemplateToPCUICExpanded]
eta_global_env [lemma, in MetaCoq.PCUIC.TemplateToPCUICExpanded]
eta2_sigma [definition, in MetaCoq.Translations.MiniHoTT]
eta2_sigma [definition, in MetaCoq.Translations.MiniHoTT_paths]
eta3_sigma [definition, in MetaCoq.Translations.MiniHoTT]
eta3_sigma [definition, in MetaCoq.Translations.MiniHoTT_paths]
ETermFlags [record, in MetaCoq.Erasure.EWellformed]
etfl:101 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
etfl:105 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
etfl:107 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
etfl:115 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
etfl:3 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
etfl:307 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
etfl:33 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
etfl:39 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
etfl:46 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
etfl:55 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
etfl:6 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
etfl:62 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
etfl:70 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
etfl:97 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
ETransform [library]
et:1145 [binder, in MetaCoq.Erasure.ErasureFunction]
et:1162 [binder, in MetaCoq.Erasure.ErasureFunction]
et:1189 [binder, in MetaCoq.Erasure.ErasureFunction]
et:1298 [binder, in MetaCoq.Erasure.ErasureFunction]
et:152 [binder, in MetaCoq.Erasure.EInlineProjections]
et:1527 [binder, in MetaCoq.Erasure.ErasureFunction]
et:159 [binder, in MetaCoq.Erasure.EDeps]
et:178 [binder, in MetaCoq.Erasure.EDeps]
et:554 [binder, in MetaCoq.Erasure.ErasureFunction]
et:856 [binder, in MetaCoq.Erasure.ErasureFunction]
et:867 [binder, in MetaCoq.Erasure.ErasureFunction]
eval [inductive, in MetaCoq.PCUIC.PCUICWcbvEval]
eval [inductive, in MetaCoq.Template.WcbvEval]
eval [abbreviation, in MetaCoq.Erasure.EWcbvEval]
eval [inductive, in MetaCoq.Erasure.EWcbvEval]
Evaluable [record, in MetaCoq.Template.Universes]
Evaluable [inductive, in MetaCoq.Template.Universes]
eval_pcuic_program [definition, in MetaCoq.PCUIC.PCUICTransform]
eval_tCase [lemma, in MetaCoq.PCUIC.PCUICProgress]
eval_opt_to_target [lemma, in MetaCoq.Erasure.EEtaExpandedFix]
eval_app_cong_mkApps [lemma, in MetaCoq.Erasure.EEtaExpandedFix]
eval_value_cong [lemma, in MetaCoq.Erasure.EEtaExpandedFix]
eval_app_cong_tApp' [lemma, in MetaCoq.Erasure.EEtaExpandedFix]
eval_stuck_fix_eq [lemma, in MetaCoq.Erasure.EEtaExpandedFix]
eval_etaexp [lemma, in MetaCoq.Erasure.EEtaExpandedFix]
eval_app_cong_tApp [lemma, in MetaCoq.Erasure.EEtaExpandedFix]
eval_tCase [lemma, in MetaCoq.Erasure.EArities]
eval_Const [lemma, in MetaCoq.PCUIC.PCUICWcbvEval]
eval_LetIn [lemma, in MetaCoq.PCUIC.PCUICWcbvEval]
eval_unique [lemma, in MetaCoq.PCUIC.PCUICWcbvEval]
eval_deterministic [lemma, in MetaCoq.PCUIC.PCUICWcbvEval]
eval_unique_sig [lemma, in MetaCoq.PCUIC.PCUICWcbvEval]
eval_mkApps_tCoFix [lemma, in MetaCoq.PCUIC.PCUICWcbvEval]
eval_tEvar [lemma, in MetaCoq.PCUIC.PCUICWcbvEval]
eval_tVar [lemma, in MetaCoq.PCUIC.PCUICWcbvEval]
eval_tRel [lemma, in MetaCoq.PCUIC.PCUICWcbvEval]
eval_closed [lemma, in MetaCoq.PCUIC.PCUICWcbvEval]
eval_stuck_fix [lemma, in MetaCoq.PCUIC.PCUICWcbvEval]
eval_mkApps_cong [lemma, in MetaCoq.PCUIC.PCUICWcbvEval]
eval_stuck_Fix [lemma, in MetaCoq.PCUIC.PCUICWcbvEval]
eval_mkApps_tInd [lemma, in MetaCoq.PCUIC.PCUICWcbvEval]
eval_mkApps_CoFix [lemma, in MetaCoq.PCUIC.PCUICWcbvEval]
eval_mkApps_Construct [lemma, in MetaCoq.PCUIC.PCUICWcbvEval]
eval_to_value [lemma, in MetaCoq.PCUIC.PCUICWcbvEval]
eval_atom [constructor, in MetaCoq.PCUIC.PCUICWcbvEval]
eval_app_cong [constructor, in MetaCoq.PCUIC.PCUICWcbvEval]
eval_construct [constructor, in MetaCoq.PCUIC.PCUICWcbvEval]
eval_cofix_proj [constructor, in MetaCoq.PCUIC.PCUICWcbvEval]
eval_cofix_case [constructor, in MetaCoq.PCUIC.PCUICWcbvEval]
eval_fix_value [constructor, in MetaCoq.PCUIC.PCUICWcbvEval]
eval_fix [constructor, in MetaCoq.PCUIC.PCUICWcbvEval]
eval_proj [constructor, in MetaCoq.PCUIC.PCUICWcbvEval]
eval_iota [constructor, in MetaCoq.PCUIC.PCUICWcbvEval]
eval_delta [constructor, in MetaCoq.PCUIC.PCUICWcbvEval]
eval_zeta [constructor, in MetaCoq.PCUIC.PCUICWcbvEval]
eval_beta [constructor, in MetaCoq.PCUIC.PCUICWcbvEval]
eval_mkApps_Construct_inv [lemma, in MetaCoq.Erasure.EConstructorsAsBlocks]
eval_etaexp [lemma, in MetaCoq.Erasure.EWcbvEvalEtaInd]
eval_preserve_mkApps_ind [lemma, in MetaCoq.Erasure.EWcbvEvalEtaInd]
eval_template_program [definition, in MetaCoq.Template.TemplateProgram]
eval_wt [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
eval_mkApps_rect [lemma, in MetaCoq.Erasure.EWcbvEvalInd]
eval_mkApps_rect.IH [variable, in MetaCoq.Erasure.EWcbvEvalInd]
eval_mkApps_rect.P [variable, in MetaCoq.Erasure.EWcbvEvalInd]
eval_mkApps_rect.Σ [variable, in MetaCoq.Erasure.EWcbvEvalInd]
eval_mkApps_rect.wfl [variable, in MetaCoq.Erasure.EWcbvEvalInd]
eval_mkApps_rect [section, in MetaCoq.Erasure.EWcbvEvalInd]
eval_proj_eval_inv_discr [lemma, in MetaCoq.Erasure.ErasureProperties]
eval_case_eval_inv_discr [lemma, in MetaCoq.Erasure.ErasureProperties]
eval_case_eval_discr [lemma, in MetaCoq.Erasure.ErasureProperties]
eval_case_tBox_inv [lemma, in MetaCoq.Erasure.ErasureProperties]
eval_empty_brs [lemma, in MetaCoq.Erasure.ErasureProperties]
eval_eprogram_env [definition, in MetaCoq.Erasure.EProgram]
eval_eprogram [definition, in MetaCoq.Erasure.EProgram]
eval_mkApps_cong [lemma, in MetaCoq.Template.WcbvEval]
eval_Const [lemma, in MetaCoq.Template.WcbvEval]
eval_LetIn [lemma, in MetaCoq.Template.WcbvEval]
eval_to_stuck_fix_inv [lemma, in MetaCoq.Template.WcbvEval]
eval_atom_inj [lemma, in MetaCoq.Template.WcbvEval]
eval_to_value [lemma, in MetaCoq.Template.WcbvEval]
eval_evals_ind [definition, in MetaCoq.Template.WcbvEval]
eval_atom [constructor, in MetaCoq.Template.WcbvEval]
eval_app_cong [constructor, in MetaCoq.Template.WcbvEval]
eval_construct [constructor, in MetaCoq.Template.WcbvEval]
eval_cofix_proj [constructor, in MetaCoq.Template.WcbvEval]
eval_cofix_case [constructor, in MetaCoq.Template.WcbvEval]
eval_fix_value [constructor, in MetaCoq.Template.WcbvEval]
eval_fix [constructor, in MetaCoq.Template.WcbvEval]
eval_proj [constructor, in MetaCoq.Template.WcbvEval]
eval_iota [constructor, in MetaCoq.Template.WcbvEval]
eval_delta [constructor, in MetaCoq.Template.WcbvEval]
eval_zeta [constructor, in MetaCoq.Template.WcbvEval]
eval_beta [constructor, in MetaCoq.Template.WcbvEval]
eval_wf [lemma, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
eval_mkApps_cong [lemma, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
eval_mkApps_fix [lemma, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
eval_mkApps_value_cong [lemma, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
eval_value_cong [lemma, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
eval_stuck_fix [lemma, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
eval_to_stuck_fix_inv [lemma, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
eval_mkApps [lemma, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
eval_tApp [lemma, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
eval_eval [lemma, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
eval_mkApps_inv [lemma, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
eval_ind_canonical [lemma, in MetaCoq.PCUIC.PCUICCanonicity]
eval_whne [lemma, in MetaCoq.PCUIC.PCUICCanonicity]
eval_box_apps [lemma, in MetaCoq.Erasure.EWcbvEval]
eval_construct_size [lemma, in MetaCoq.Erasure.EWcbvEval]
eval_mkApps_Construct_size [lemma, in MetaCoq.Erasure.EWcbvEval]
eval_mkApps_inv_size [lemma, in MetaCoq.Erasure.EWcbvEval]
eval_mkApps_Construct_block_inv [lemma, in MetaCoq.Erasure.EWcbvEval]
eval_mkApps_Construct_inv [lemma, in MetaCoq.Erasure.EWcbvEval]
eval_mkApps_inv' [lemma, in MetaCoq.Erasure.EWcbvEval]
eval_mkApps_tFix_inv_size_unguarded [lemma, in MetaCoq.Erasure.EWcbvEval]
eval_mkApps_tFix_inv_size [lemma, in MetaCoq.Erasure.EWcbvEval]
eval_wellformed [lemma, in MetaCoq.Erasure.EWcbvEval]
eval_closed [lemma, in MetaCoq.Erasure.EWcbvEval]
eval_depth [definition, in MetaCoq.Erasure.EWcbvEval]
eval_nondep [definition, in MetaCoq.Erasure.EWcbvEval]
eval_mkApps_inv [lemma, in MetaCoq.Erasure.EWcbvEval]
eval_trans [lemma, in MetaCoq.Erasure.EWcbvEval]
eval_trans' [lemma, in MetaCoq.Erasure.EWcbvEval]
eval_deterministic_all [lemma, in MetaCoq.Erasure.EWcbvEval]
eval_deterministic [lemma, in MetaCoq.Erasure.EWcbvEval]
eval_unique [lemma, in MetaCoq.Erasure.EWcbvEval]
eval_unique_sig [lemma, in MetaCoq.Erasure.EWcbvEval]
eval_mkApps_cong [lemma, in MetaCoq.Erasure.EWcbvEval]
eval_mkApps_tBox [lemma, in MetaCoq.Erasure.EWcbvEval]
eval_mkApps_CoFix [lemma, in MetaCoq.Erasure.EWcbvEval]
eval_mkApps_Construct_block [lemma, in MetaCoq.Erasure.EWcbvEval]
eval_mkApps_Construct [lemma, in MetaCoq.Erasure.EWcbvEval]
eval_stuck_Fix [lemma, in MetaCoq.Erasure.EWcbvEval]
eval_to_mkApps_tBox_inv [lemma, in MetaCoq.Erasure.EWcbvEval]
eval_mkApps_tFix_inv [lemma, in MetaCoq.Erasure.EWcbvEval]
eval_mkApps_tCoFix [lemma, in MetaCoq.Erasure.EWcbvEval]
eval_to_value [lemma, in MetaCoq.Erasure.EWcbvEval]
eval_Construct_inv [lemma, in MetaCoq.Erasure.EWcbvEval]
eval_atom [constructor, in MetaCoq.Erasure.EWcbvEval]
eval_app_cong [constructor, in MetaCoq.Erasure.EWcbvEval]
eval_construct_block [constructor, in MetaCoq.Erasure.EWcbvEval]
eval_construct [constructor, in MetaCoq.Erasure.EWcbvEval]
eval_proj_prop [constructor, in MetaCoq.Erasure.EWcbvEval]
eval_proj_block [constructor, in MetaCoq.Erasure.EWcbvEval]
eval_proj [constructor, in MetaCoq.Erasure.EWcbvEval]
eval_delta [constructor, in MetaCoq.Erasure.EWcbvEval]
eval_cofix_proj [constructor, in MetaCoq.Erasure.EWcbvEval]
eval_cofix_case [constructor, in MetaCoq.Erasure.EWcbvEval]
eval_fix' [constructor, in MetaCoq.Erasure.EWcbvEval]
eval_fix_value [constructor, in MetaCoq.Erasure.EWcbvEval]
eval_fix [constructor, in MetaCoq.Erasure.EWcbvEval]
eval_iota_sing [constructor, in MetaCoq.Erasure.EWcbvEval]
eval_iota_block [constructor, in MetaCoq.Erasure.EWcbvEval]
eval_iota [constructor, in MetaCoq.Erasure.EWcbvEval]
eval_zeta [constructor, in MetaCoq.Erasure.EWcbvEval]
eval_beta [constructor, in MetaCoq.Erasure.EWcbvEval]
eval_box [constructor, in MetaCoq.Erasure.EWcbvEval]
eval_is_box [lemma, in MetaCoq.Erasure.EOptimizePropDiscr]
eval'':49 [binder, in MetaCoq.Template.Transform]
eval':13 [binder, in MetaCoq.Template.Transform]
eval':40 [binder, in MetaCoq.Template.Transform]
eval':48 [binder, in MetaCoq.Template.Transform]
eval:12 [binder, in MetaCoq.Template.Transform]
eval:39 [binder, in MetaCoq.Template.Transform]
eval:47 [binder, in MetaCoq.Template.Transform]
evar_red [constructor, in MetaCoq.Template.Typing]
evar_pred [constructor, in MetaCoq.PCUIC.PCUICParallelReduction]
evar_red [constructor, in MetaCoq.PCUIC.PCUICReduction]
eva:432 [binder, in MetaCoq.Erasure.EWcbvEval]
eva:445 [binder, in MetaCoq.Erasure.EWcbvEval]
eva:467 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
even [definition, in MetaCoq.Examples.demo]
even':43 [binder, in MetaCoq.Examples.add_constructor]
even':45 [binder, in MetaCoq.Examples.add_constructor]
evf:429 [binder, in MetaCoq.Erasure.EWcbvEval]
evf:442 [binder, in MetaCoq.Erasure.EWcbvEval]
evres:433 [binder, in MetaCoq.Erasure.EWcbvEval]
ev':230 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
ev':285 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
ev':288 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
ev':456 [binder, in MetaCoq.Erasure.EWcbvEval]
ev':9 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
ev':95 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
ev1:289 [binder, in MetaCoq.Erasure.EWcbvEval]
ev1:293 [binder, in MetaCoq.Erasure.EWcbvEval]
ev1:380 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
ev1:387 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
ev2:290 [binder, in MetaCoq.Erasure.EWcbvEval]
ev2:294 [binder, in MetaCoq.Erasure.EWcbvEval]
ev2:381 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
ev2:388 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
ev:1144 [binder, in MetaCoq.PCUIC.PCUICReduction]
ev:1157 [binder, in MetaCoq.PCUIC.PCUICReduction]
ev:116 [binder, in MetaCoq.PCUIC.PCUICReduction]
ev:1225 [binder, in MetaCoq.PCUIC.PCUICConversion]
ev:1228 [binder, in MetaCoq.PCUIC.PCUICConversion]
ev:13 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
ev:13 [binder, in MetaCoq.Template.Checker]
ev:16 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
ev:16 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
ev:160 [binder, in MetaCoq.Template.EtaExpand]
ev:166 [binder, in MetaCoq.SafeChecker.PCUICErrors]
ev:181 [binder, in MetaCoq.Template.Ast]
ev:187 [binder, in MetaCoq.Erasure.EEtaExpanded]
ev:20 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
ev:210 [binder, in MetaCoq.Template.Typing]
ev:220 [binder, in MetaCoq.Erasure.EEtaExpanded]
ev:227 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
ev:258 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
ev:289 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
ev:290 [binder, in MetaCoq.PCUIC.PCUICReduction]
ev:321 [binder, in MetaCoq.Erasure.EWcbvEval]
ev:397 [binder, in MetaCoq.Template.Typing]
ev:422 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
ev:426 [binder, in MetaCoq.Erasure.EWcbvEval]
ev:440 [binder, in MetaCoq.Erasure.EWcbvEval]
ev:452 [binder, in MetaCoq.Erasure.EWcbvEval]
ev:470 [binder, in MetaCoq.PCUIC.PCUICSR]
ev:494 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
ev:57 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
ev:6 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
ev:74 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
ev:76 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
ev:84 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
ev:94 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
ev:95 [binder, in MetaCoq.Template.EtaExpand]
EWcbvEval [library]
EWcbvEvalEtaInd [library]
EWcbvEvalInd [library]
EWellformed [library]
EWtAst [library]
exists_neg_forall [lemma, in MetaCoq.Template.common.uGraph]
exist_irrel_eq [lemma, in MetaCoq.PCUIC.utils.PCUICPrimitive]
expand [abbreviation, in MetaCoq.SafeChecker.PCUICSafeConversion]
expanded [inductive, in MetaCoq.Template.EtaExpand]
expanded [section, in MetaCoq.Template.EtaExpand]
expanded [inductive, in MetaCoq.Erasure.EEtaExpandedFix]
expanded [section, in MetaCoq.Erasure.EEtaExpandedFix]
expanded [inductive, in MetaCoq.PCUIC.PCUICEtaExpand]
expanded [section, in MetaCoq.PCUIC.PCUICEtaExpand]
expanded [inductive, in MetaCoq.Erasure.EEtaExpanded]
expanded [section, in MetaCoq.Erasure.EEtaExpanded]
expanded_decl_env_irrel [lemma, in MetaCoq.Template.EtaExpand]
expanded_context_env_irrel [lemma, in MetaCoq.Template.EtaExpand]
expanded_env_irrel [lemma, in MetaCoq.Template.EtaExpand]
expanded_eta_single_tRel_app [lemma, in MetaCoq.Template.EtaExpand]
expanded_lift' [lemma, in MetaCoq.Template.EtaExpand]
expanded_lift [lemma, in MetaCoq.Template.EtaExpand]
expanded_unlift [lemma, in MetaCoq.Template.EtaExpand]
expanded_mkApps [lemma, in MetaCoq.Template.EtaExpand]
expanded_mkApps_inv [lemma, in MetaCoq.Template.EtaExpand]
expanded_tApps_inv [lemma, in MetaCoq.Template.EtaExpand]
expanded_tApp_args [lemma, in MetaCoq.Template.EtaExpand]
expanded_mkApps_tFix_inv [lemma, in MetaCoq.Template.EtaExpand]
expanded_mkApps_tFix [lemma, in MetaCoq.Template.EtaExpand]
expanded_mkApps_tConstruct [lemma, in MetaCoq.Template.EtaExpand]
expanded_fold_lambda [lemma, in MetaCoq.Template.EtaExpand]
expanded_program [definition, in MetaCoq.Template.EtaExpand]
expanded_global_env [definition, in MetaCoq.Template.EtaExpand]
expanded_global_cons [constructor, in MetaCoq.Template.EtaExpand]
expanded_global_nil [constructor, in MetaCoq.Template.EtaExpand]
expanded_global_declarations [inductive, in MetaCoq.Template.EtaExpand]
expanded_decl [definition, in MetaCoq.Template.EtaExpand]
expanded_ind_bodies [projection, in MetaCoq.Template.EtaExpand]
expanded_params [projection, in MetaCoq.Template.EtaExpand]
expanded_minductive_decl [record, in MetaCoq.Template.EtaExpand]
expanded_ind_ctors [projection, in MetaCoq.Template.EtaExpand]
expanded_inductive_decl [record, in MetaCoq.Template.EtaExpand]
expanded_cstr_type [projection, in MetaCoq.Template.EtaExpand]
expanded_cstr_args [projection, in MetaCoq.Template.EtaExpand]
expanded_constructor_decl [record, in MetaCoq.Template.EtaExpand]
expanded_context [definition, in MetaCoq.Template.EtaExpand]
expanded_body [projection, in MetaCoq.Template.EtaExpand]
expanded_constant_decl [record, in MetaCoq.Template.EtaExpand]
expanded_ind [lemma, in MetaCoq.Template.EtaExpand]
expanded_tConstruct_app [constructor, in MetaCoq.Template.EtaExpand]
expanded_tCoFix [constructor, in MetaCoq.Template.EtaExpand]
expanded_tFix [constructor, in MetaCoq.Template.EtaExpand]
expanded_tProj [constructor, in MetaCoq.Template.EtaExpand]
expanded_tCase [constructor, in MetaCoq.Template.EtaExpand]
expanded_tConstruct [constructor, in MetaCoq.Template.EtaExpand]
expanded_tInd [constructor, in MetaCoq.Template.EtaExpand]
expanded_tConst [constructor, in MetaCoq.Template.EtaExpand]
expanded_tApp [constructor, in MetaCoq.Template.EtaExpand]
expanded_tLetIn [constructor, in MetaCoq.Template.EtaExpand]
expanded_tLambda [constructor, in MetaCoq.Template.EtaExpand]
expanded_tProd [constructor, in MetaCoq.Template.EtaExpand]
expanded_tCast [constructor, in MetaCoq.Template.EtaExpand]
expanded_tSort [constructor, in MetaCoq.Template.EtaExpand]
expanded_tEvar [constructor, in MetaCoq.Template.EtaExpand]
expanded_tVar [constructor, in MetaCoq.Template.EtaExpand]
expanded_tRel_app [constructor, in MetaCoq.Template.EtaExpand]
expanded_tRel [constructor, in MetaCoq.Template.EtaExpand]
expanded_global_env_isEtaExp_env [lemma, in MetaCoq.Erasure.EEtaExpandedFix]
expanded_isEtaExp [lemma, in MetaCoq.Erasure.EEtaExpandedFix]
expanded_isEtaExp_app_ [lemma, in MetaCoq.Erasure.EEtaExpandedFix]
expanded_weakening [lemma, in MetaCoq.Erasure.EEtaExpandedFix]
expanded_head_viewc [definition, in MetaCoq.Erasure.EEtaExpandedFix]
expanded_head_other [constructor, in MetaCoq.Erasure.EEtaExpandedFix]
expanded_head_rel [constructor, in MetaCoq.Erasure.EEtaExpandedFix]
expanded_head_fix [constructor, in MetaCoq.Erasure.EEtaExpandedFix]
expanded_head_construct [constructor, in MetaCoq.Erasure.EEtaExpandedFix]
expanded_head_view [inductive, in MetaCoq.Erasure.EEtaExpandedFix]
expanded_closed [lemma, in MetaCoq.Erasure.EEtaExpandedFix]
expanded_eprogram_env [definition, in MetaCoq.Erasure.EEtaExpandedFix]
expanded_eprogram [definition, in MetaCoq.Erasure.EEtaExpandedFix]
expanded_global_env [definition, in MetaCoq.Erasure.EEtaExpandedFix]
expanded_global_cons [constructor, in MetaCoq.Erasure.EEtaExpandedFix]
expanded_global_nil [constructor, in MetaCoq.Erasure.EEtaExpandedFix]
expanded_global_declarations [inductive, in MetaCoq.Erasure.EEtaExpandedFix]
expanded_decl [definition, in MetaCoq.Erasure.EEtaExpandedFix]
expanded_constant_decl [definition, in MetaCoq.Erasure.EEtaExpandedFix]
expanded_ind [lemma, in MetaCoq.Erasure.EEtaExpandedFix]
expanded_tBox [constructor, in MetaCoq.Erasure.EEtaExpandedFix]
expanded_tConstruct_app [constructor, in MetaCoq.Erasure.EEtaExpandedFix]
expanded_tCoFix [constructor, in MetaCoq.Erasure.EEtaExpandedFix]
expanded_tFix [constructor, in MetaCoq.Erasure.EEtaExpandedFix]
expanded_tProj [constructor, in MetaCoq.Erasure.EEtaExpandedFix]
expanded_tCase [constructor, in MetaCoq.Erasure.EEtaExpandedFix]
expanded_tConst [constructor, in MetaCoq.Erasure.EEtaExpandedFix]
expanded_mkApps [constructor, in MetaCoq.Erasure.EEtaExpandedFix]
expanded_tLetIn [constructor, in MetaCoq.Erasure.EEtaExpandedFix]
expanded_tLambda [constructor, in MetaCoq.Erasure.EEtaExpandedFix]
expanded_tEvar [constructor, in MetaCoq.Erasure.EEtaExpandedFix]
expanded_tVar [constructor, in MetaCoq.Erasure.EEtaExpandedFix]
expanded_tRel_app [constructor, in MetaCoq.Erasure.EEtaExpandedFix]
expanded_erases [lemma, in MetaCoq.Erasure.ErasureCorrectness]
expanded_weakening [lemma, in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_subst_instance [lemma, in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_let_expansion [lemma, in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_subst [lemma, in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_lift [lemma, in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_mkApps_expanded [lemma, in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_pcuic_program [definition, in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_global_env [definition, in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_global_cons [constructor, in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_global_nil [constructor, in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_global_declarations [inductive, in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_decl [definition, in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_ind_bodies [projection, in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_params [projection, in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_minductive_decl [record, in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_ind_ctors [projection, in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_inductive_decl [record, in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_cstr_args [projection, in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_constructor_decl [record, in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_body [projection, in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_constant_decl [record, in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_ind [lemma, in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_context [definition, in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_tConstruct_app [constructor, in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_tCoFix [constructor, in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_tFix [constructor, in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_tProj [constructor, in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_tCase [constructor, in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_tInd [constructor, in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_tConst [constructor, in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_mkApps [constructor, in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_tLetIn [constructor, in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_tLambda [constructor, in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_tProd [constructor, in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_tSort [constructor, in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_tEvar [constructor, in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_tVar [constructor, in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_tRel [constructor, in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_expand_lets_program [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
expanded_global_env_expand_lets [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
expanded_smash_context [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
expanded_trans_local [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
expanded_expand_lets [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
expanded_erase_fast [lemma, in MetaCoq.Erasure.ErasureFunction]
expanded_erase_global_fast [lemma, in MetaCoq.Erasure.ErasureFunction]
expanded_erase_global [lemma, in MetaCoq.Erasure.ErasureFunction]
expanded_erase [lemma, in MetaCoq.Erasure.ErasureFunction]
expanded_weakening_global [lemma, in MetaCoq.Erasure.ErasureFunction]
expanded_eprogram_env_expanded_eprogram_cstrs [lemma, in MetaCoq.Erasure.ETransform]
expanded_erase_program [lemma, in MetaCoq.Erasure.ETransform]
expanded_mkApps_expanded [lemma, in MetaCoq.Erasure.EEtaExpanded]
expanded_global_env_isEtaExp_env [lemma, in MetaCoq.Erasure.EEtaExpanded]
expanded_isEtaExp [lemma, in MetaCoq.Erasure.EEtaExpanded]
expanded_isEtaExp_app_ [lemma, in MetaCoq.Erasure.EEtaExpanded]
expanded_eprogram_env_cstrs [definition, in MetaCoq.Erasure.EEtaExpanded]
expanded_eprogram_cstrs [definition, in MetaCoq.Erasure.EEtaExpanded]
expanded_global_env [definition, in MetaCoq.Erasure.EEtaExpanded]
expanded_global_cons [constructor, in MetaCoq.Erasure.EEtaExpanded]
expanded_global_nil [constructor, in MetaCoq.Erasure.EEtaExpanded]
expanded_global_declarations [inductive, in MetaCoq.Erasure.EEtaExpanded]
expanded_decl [definition, in MetaCoq.Erasure.EEtaExpanded]
expanded_constant_decl [definition, in MetaCoq.Erasure.EEtaExpanded]
expanded_ind [lemma, in MetaCoq.Erasure.EEtaExpanded]
expanded_tBox [constructor, in MetaCoq.Erasure.EEtaExpanded]
expanded_tConstruct_app [constructor, in MetaCoq.Erasure.EEtaExpanded]
expanded_tCoFix [constructor, in MetaCoq.Erasure.EEtaExpanded]
expanded_tFix [constructor, in MetaCoq.Erasure.EEtaExpanded]
expanded_tProj [constructor, in MetaCoq.Erasure.EEtaExpanded]
expanded_tCase [constructor, in MetaCoq.Erasure.EEtaExpanded]
expanded_tConst [constructor, in MetaCoq.Erasure.EEtaExpanded]
expanded_mkApps [constructor, in MetaCoq.Erasure.EEtaExpanded]
expanded_tLetIn [constructor, in MetaCoq.Erasure.EEtaExpanded]
expanded_tLambda [constructor, in MetaCoq.Erasure.EEtaExpanded]
expanded_tEvar [constructor, in MetaCoq.Erasure.EEtaExpanded]
expanded_tVar [constructor, in MetaCoq.Erasure.EEtaExpanded]
expanded_tRel [constructor, in MetaCoq.Erasure.EEtaExpanded]
expanded_trans_program [lemma, in MetaCoq.PCUIC.TemplateToPCUICExpanded]
expanded_trans_global_env [lemma, in MetaCoq.PCUIC.TemplateToPCUICExpanded]
expanded_trans_local [lemma, in MetaCoq.PCUIC.TemplateToPCUICExpanded]
expanded_bcontext [lemma, in MetaCoq.PCUIC.TemplateToPCUICExpanded]
expanded_context_weakening [lemma, in MetaCoq.PCUIC.TemplateToPCUICExpanded]
expanded_weakening [lemma, in MetaCoq.PCUIC.TemplateToPCUICExpanded]
expanded_inds [lemma, in MetaCoq.PCUIC.TemplateToPCUICExpanded]
expanded_context_subst [lemma, in MetaCoq.PCUIC.TemplateToPCUICExpanded]
expanded_let_expansion [lemma, in MetaCoq.PCUIC.TemplateToPCUICExpanded]
expanded_extended_subst [lemma, in MetaCoq.PCUIC.TemplateToPCUICExpanded]
expanded_context_map2_bias_left [lemma, in MetaCoq.PCUIC.TemplateToPCUICExpanded]
expanded.Σ [variable, in MetaCoq.Template.EtaExpand]
expanded.Σ [variable, in MetaCoq.Erasure.EEtaExpandedFix]
expanded.Σ [variable, in MetaCoq.PCUIC.PCUICEtaExpand]
expanded.Σ [variable, in MetaCoq.Erasure.EEtaExpanded]
expand_lets_program [definition, in MetaCoq.PCUIC.PCUICExpandLets]
expand_lets_subst_comm' [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
expand_lets_eq [lemma, in MetaCoq.Template.TermEquality]
expand_lets_ctx_app [lemma, in MetaCoq.PCUIC.PCUICInductives]
expand_lets_k_0 [lemma, in MetaCoq.PCUIC.PCUICInductives]
expand_lets_k_to_extended_list_k [lemma, in MetaCoq.PCUIC.PCUICInductives]
expand_lets_k_subst_comm [lemma, in MetaCoq.PCUIC.PCUICInductives]
expand_lets_ctx_tip [lemma, in MetaCoq.PCUIC.PCUICInductives]
expand_lets_ctx_snoc [lemma, in MetaCoq.PCUIC.PCUICInductives]
expand_lets_k_ctx_snoc [lemma, in MetaCoq.PCUIC.PCUICInductives]
expand_lets_ctx_lift [lemma, in MetaCoq.PCUIC.PCUICInductives]
expand_lets_lift [lemma, in MetaCoq.PCUIC.PCUICInductives]
expand_lets_app [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
expand_lets_k_app [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
expand_lets_subst_comm [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
expand_lets_ctx_assumption_context [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
expand_lets_assumption_context [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
expand_lets_tRel [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
expand_lets_mkApps [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
expand_lets_k_mkApps [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
expand_lets_it_mkProd_or_LetIn [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
expand_lets_nil [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
expand_lets_k_ctx_decl [definition, in MetaCoq.PCUIC.PCUICSigmaCalculus]
expand_lets_k_ctx_vass [definition, in MetaCoq.PCUIC.PCUICSigmaCalculus]
expand_lets_vdef [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
expand_lets_k_vdef [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
expand_lets_vass [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
expand_lets_k_vass [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
expand_lets_sound [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_expand_lets [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_smash_context_id [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_ctx_lift_context_cancel [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_comm [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_k_lift [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_set_binder_name [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_k_subst_comm [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_subst_comm [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_lift_cancel [lemma, in MetaCoq.PCUIC.PCUICSR]
expand_lets_eq_map [lemma, in MetaCoq.PCUIC.PCUICSR]
expand_lets_eq [lemma, in MetaCoq.PCUIC.PCUICSR]
expand_lets_subst_instance [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
expand_lets_ctx_nil [lemma, in MetaCoq.PCUIC.PCUICContexts]
expand_lets_k_ctx_nil [lemma, in MetaCoq.PCUIC.PCUICContexts]
expand_lets_smash_context [lemma, in MetaCoq.PCUIC.PCUICContexts]
expand_lets_k_ctx_subst_id' [lemma, in MetaCoq.PCUIC.PCUICSpine]
expand_lets_ctx_o_lets [lemma, in MetaCoq.PCUIC.PCUICSpine]
expand_lets_erasure [lemma, in MetaCoq.Erasure.Prelim]
exprs:111 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
exprs:27 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
exprs:49 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
expr_set_forall_map [lemma, in MetaCoq.PCUIC.PCUICCumulProp]
expr_gc_declared_declared [lemma, in MetaCoq.Template.common.uGraph]
expr:19 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
extended_subst_shiftn_impl [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
extended_subst_shiftn_aboveP [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
extended_subst_shiftn [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
extended_subst_lift_context [lemma, in MetaCoq.PCUIC.PCUICInductives]
extended_subst_set_binder_name [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
extended_subst_app [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
extended_subst_to_extended_list_k [lemma, in MetaCoq.PCUIC.PCUICContexts]
extendP [definition, in MetaCoq.PCUIC.PCUICParallelReduction]
extends [definition, in MetaCoq.Erasure.EGlobalEnv]
ExtendsWf [section, in MetaCoq.PCUIC.PCUICWeakeningEnv]
ExtendsWf [section, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
ExtendsWf.wf [variable, in MetaCoq.PCUIC.PCUICWeakeningEnv]
ExtendsWf.wf [variable, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
extends_decls_wf [lemma, in MetaCoq.PCUIC.PCUICWeakeningEnv]
extends_lookup [lemma, in MetaCoq.PCUIC.PCUICWeakeningEnv]
extends_wf_universe [lemma, in MetaCoq.PCUIC.PCUICWeakeningEnv]
extends_trans [lemma, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
extends_trans_global_decls_acc [lemma, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
extends_lookup_projection [lemma, in MetaCoq.Erasure.EInlineProjections]
extends_decls_trans [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
extends_trans [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
extends_lookup_env [lemma, in MetaCoq.Erasure.ErasureFunction]
extends_wf_global_decl [lemma, in MetaCoq.Erasure.EWellformed]
extends_wellformed [lemma, in MetaCoq.Erasure.EWellformed]
extends_is_propositional [lemma, in MetaCoq.Erasure.EWellformed]
extends_constructor_isprop_pars_decl [lemma, in MetaCoq.Erasure.EWellformed]
extends_lookup_constructor [lemma, in MetaCoq.Erasure.EWellformed]
extends_lookup [lemma, in MetaCoq.Erasure.EWellformed]
extends_wf_glob [lemma, in MetaCoq.Erasure.EExtends]
extends_decls_trans [lemma, in MetaCoq.PCUIC.TemplateToPCUICExpanded]
extends_lookup_inductive_pars [lemma, in MetaCoq.Erasure.ERemoveParams]
extends_lookup_projection [lemma, in MetaCoq.Erasure.EGenericMapEnv]
extends_inductive_isprop_and_pars [lemma, in MetaCoq.Erasure.EOptimizePropDiscr]
extends_wf_cofixpoint [lemma, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
extends_wf_fixpoint [lemma, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
extends_check_recursivity_kind [lemma, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
extends_wf_local [lemma, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
extend_over [definition, in MetaCoq.PCUIC.PCUICParallelReduction]
Extract [library]
Extractable [library]
ExtractableLoader [library]
Extraction [library]
Extraction [library]
Extraction [library]
Extraction [library]
extraction_checker_flags [instance, in MetaCoq.Template.config]
extraction_normalizing [instance, in MetaCoq.PCUIC.PCUICSN]
extract_form [definition, in MetaCoq.Examples.tauto]
ext_lift [lemma, in MetaCoq.Template.EtaExpand]
ext:106 [binder, in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
ext:1070 [binder, in MetaCoq.Template.utils.wGraph]
ext:1097 [binder, in MetaCoq.Template.utils.wGraph]
ext:1124 [binder, in MetaCoq.Template.utils.wGraph]
ext:255 [binder, in MetaCoq.PCUIC.PCUICSpine]
ext:555 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
ext:74 [binder, in MetaCoq.PCUIC.PCUICSpine]
ext:776 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
ext:91 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
ext:96 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
e'':303 [binder, in MetaCoq.Erasure.EWcbvEval]
e'':306 [binder, in MetaCoq.Erasure.EWcbvEval]
e':107 [binder, in MetaCoq.Template.Universes]
E':116 [binder, in MetaCoq.Translations.translation_utils]
E':124 [binder, in MetaCoq.Translations.translation_utils]
E':132 [binder, in MetaCoq.Translations.translation_utils]
E':150 [binder, in MetaCoq.Translations.translation_utils]
E':152 [binder, in MetaCoq.Translations.translation_utils]
E':157 [binder, in MetaCoq.Translations.translation_utils]
E':159 [binder, in MetaCoq.Translations.translation_utils]
e':210 [binder, in MetaCoq.Erasure.EWcbvEval]
e':217 [binder, in MetaCoq.Translations.times_bool_fun]
e':251 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
e':293 [binder, in MetaCoq.Template.WcbvEval]
e':302 [binder, in MetaCoq.Erasure.EWcbvEval]
e':305 [binder, in MetaCoq.Erasure.EWcbvEval]
e':310 [binder, in MetaCoq.Template.utils.wGraph]
e':323 [binder, in MetaCoq.Template.common.uGraph]
e':328 [binder, in MetaCoq.Template.common.uGraph]
e':368 [binder, in MetaCoq.Template.common.uGraph]
e':600 [binder, in MetaCoq.Template.common.uGraph]
e':604 [binder, in MetaCoq.Template.common.uGraph]
e':609 [binder, in MetaCoq.Template.common.uGraph]
E':62 [binder, in MetaCoq.Translations.translation_utils]
E':64 [binder, in MetaCoq.Translations.translation_utils]
E':71 [binder, in MetaCoq.Translations.translation_utils]
E':73 [binder, in MetaCoq.Translations.translation_utils]
E':83 [binder, in MetaCoq.Translations.translation_utils]
E':85 [binder, in MetaCoq.Translations.translation_utils]
E':99 [binder, in MetaCoq.Translations.translation_utils]
e0:124 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
e0:126 [binder, in MetaCoq.Template.Universes]
e0:136 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
e0:153 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
e0:167 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
e0:169 [binder, in MetaCoq.Template.Universes]
e0:171 [binder, in MetaCoq.Template.Universes]
e0:177 [binder, in MetaCoq.Template.Universes]
e0:177 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
e0:179 [binder, in MetaCoq.Template.Universes]
e0:183 [binder, in MetaCoq.Erasure.EWcbvEval]
e0:36 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
e0:52 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
e0:784 [binder, in MetaCoq.Template.utils.wGraph]
e1:125 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
e1:128 [binder, in MetaCoq.PCUIC.utils.PCUICUtils]
e1:137 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
e1:154 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
e1:169 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
e1:197 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
e1:206 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
e1:218 [binder, in MetaCoq.Translations.times_bool_fun]
e1:219 [binder, in MetaCoq.Translations.times_bool_fun]
e1:237 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
e1:246 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
e1:255 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
e1:262 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
e1:271 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
e1:278 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
e1:287 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
e1:294 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
e1:3004 [binder, in MetaCoq.Translations.MiniHoTT]
e1:303 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
e1:310 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
e1:317 [binder, in MetaCoq.Template.common.uGraph]
e1:332 [binder, in MetaCoq.Template.common.uGraph]
e1:337 [binder, in MetaCoq.Template.common.uGraph]
e1:37 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
e1:398 [binder, in MetaCoq.Template.common.uGraph]
e1:406 [binder, in MetaCoq.Template.common.uGraph]
e1:486 [binder, in MetaCoq.Template.common.uGraph]
e1:53 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
e1:86 [binder, in MetaCoq.PCUIC.utils.PCUICUtils]
e2:126 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
e2:129 [binder, in MetaCoq.PCUIC.utils.PCUICUtils]
e2:138 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
e2:156 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
e2:170 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
e2:220 [binder, in MetaCoq.Translations.times_bool_fun]
e2:221 [binder, in MetaCoq.Translations.times_bool_fun]
e2:3005 [binder, in MetaCoq.Translations.MiniHoTT]
e2:318 [binder, in MetaCoq.Template.common.uGraph]
e2:335 [binder, in MetaCoq.Template.common.uGraph]
e2:38 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
e2:54 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
e2:87 [binder, in MetaCoq.PCUIC.utils.PCUICUtils]
e3:127 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
e3:139 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
e3:39 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
e3:55 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
e4:128 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
e4:140 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
e4:40 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
e4:56 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
e5:41 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
e5:57 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
e:10 [binder, in MetaCoq.Template.BasicAst]
e:10 [binder, in MetaCoq.PCUIC.utils.PCUICPrimitive]
e:101 [binder, in MetaCoq.Template.Universes]
E:101 [binder, in MetaCoq.Template.monad_utils]
e:1012 [binder, in MetaCoq.Template.utils.wGraph]
e:1015 [binder, in MetaCoq.Template.utils.wGraph]
e:103 [binder, in MetaCoq.Template.Universes]
e:1030 [binder, in MetaCoq.Template.utils.wGraph]
e:1038 [binder, in MetaCoq.Template.utils.wGraph]
e:105 [binder, in MetaCoq.Template.Universes]
e:107 [binder, in MetaCoq.Translations.translation_utils]
e:1073 [binder, in MetaCoq.Template.utils.wGraph]
e:108 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
e:1080 [binder, in MetaCoq.Template.utils.wGraph]
e:1083 [binder, in MetaCoq.Template.utils.wGraph]
e:1084 [binder, in MetaCoq.Erasure.ErasureFunction]
e:1088 [binder, in MetaCoq.Template.utils.wGraph]
e:1088 [binder, in MetaCoq.Erasure.ErasureFunction]
e:109 [binder, in MetaCoq.Template.Universes]
e:1091 [binder, in MetaCoq.Template.utils.wGraph]
e:1092 [binder, in MetaCoq.Template.utils.wGraph]
e:1093 [binder, in MetaCoq.Template.utils.wGraph]
e:1093 [binder, in MetaCoq.Erasure.ErasureFunction]
e:1097 [binder, in MetaCoq.Erasure.ErasureFunction]
E:11 [binder, in MetaCoq.Translations.param_cheap_packed]
e:1101 [binder, in MetaCoq.Erasure.ErasureFunction]
e:1105 [binder, in MetaCoq.Erasure.ErasureFunction]
e:1109 [binder, in MetaCoq.Erasure.ErasureFunction]
e:1114 [binder, in MetaCoq.Erasure.ErasureFunction]
e:1118 [binder, in MetaCoq.Erasure.ErasureFunction]
e:112 [binder, in MetaCoq.Template.Universes]
e:1122 [binder, in MetaCoq.Erasure.ErasureFunction]
e:114 [binder, in MetaCoq.Template.Universes]
e:117 [binder, in MetaCoq.Erasure.ErasureProperties]
e:117 [binder, in MetaCoq.Template.Pretty]
e:118 [binder, in MetaCoq.Template.Universes]
e:119 [binder, in MetaCoq.PCUIC.utils.PCUICUtils]
e:120 [binder, in MetaCoq.Template.Universes]
e:122 [binder, in MetaCoq.PCUIC.PCUICEquality]
e:123 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
e:124 [binder, in MetaCoq.PCUIC.utils.PCUICUtils]
e:125 [binder, in MetaCoq.Template.Universes]
e:126 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
E:127 [binder, in MetaCoq.Template.monad_utils]
e:13 [binder, in MetaCoq.Examples.metacoq_tour]
e:13 [binder, in MetaCoq.Template.EnvMap]
e:130 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
e:130 [binder, in MetaCoq.Template.monad_utils]
e:133 [binder, in MetaCoq.PCUIC.utils.PCUICUtils]
e:1333 [binder, in MetaCoq.Template.Typing]
e:1335 [binder, in MetaCoq.Template.Typing]
e:1337 [binder, in MetaCoq.Template.Typing]
e:1339 [binder, in MetaCoq.Template.Typing]
E:134 [binder, in MetaCoq.Translations.param_cheap_packed]
e:135 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
E:135 [binder, in MetaCoq.Template.monad_utils]
e:138 [binder, in MetaCoq.SafeChecker.PCUICErrors]
e:139 [binder, in MetaCoq.Template.monad_utils]
e:14 [binder, in MetaCoq.SafeChecker.PCUICErrors]
E:140 [binder, in MetaCoq.Translations.param_cheap_packed]
e:141 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
E:142 [binder, in MetaCoq.Template.monad_utils]
E:145 [binder, in MetaCoq.Translations.param_cheap_packed]
e:146 [binder, in MetaCoq.Template.Universes]
E:147 [binder, in MetaCoq.Translations.param_cheap_packed]
e:147 [binder, in MetaCoq.Template.monad_utils]
e:149 [binder, in MetaCoq.SafeChecker.PCUICErrors]
E:15 [binder, in MetaCoq.Translations.times_bool_fun]
e:150 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
e:151 [binder, in MetaCoq.Template.Universes]
e:152 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
e:153 [binder, in MetaCoq.Erasure.ErasureProperties]
e:1545 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
e:156 [binder, in MetaCoq.Template.Universes]
e:157 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
e:159 [binder, in MetaCoq.Erasure.ErasureProperties]
e:16 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
e:1609 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
e:161 [binder, in MetaCoq.Template.Universes]
e:163 [binder, in MetaCoq.Erasure.ErasureProperties]
e:165 [binder, in MetaCoq.Template.Universes]
e:166 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
e:168 [binder, in MetaCoq.Template.Universes]
E:17 [binder, in MetaCoq.Translations.param_cheap_packed]
e:17 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
E:17 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
e:172 [binder, in MetaCoq.Erasure.ErasureProperties]
e:1731 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
e:175 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
e:175 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
e:176 [binder, in MetaCoq.Template.Universes]
e:176 [binder, in MetaCoq.Template.common.uGraph]
e:179 [binder, in MetaCoq.SafeChecker.PCUICErrors]
e:179 [binder, in MetaCoq.Erasure.ErasureProperties]
E:18 [binder, in MetaCoq.Translations.param_generous_packed]
e:182 [binder, in MetaCoq.Erasure.EWcbvEval]
E:183 [binder, in MetaCoq.Translations.MiniHoTT]
e:184 [binder, in MetaCoq.Template.Universes]
e:184 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
e:186 [binder, in MetaCoq.Erasure.ErasureProperties]
e:188 [binder, in MetaCoq.Template.Universes]
e:189 [binder, in MetaCoq.Template.Universes]
e:191 [binder, in MetaCoq.Template.Universes]
e:191 [binder, in MetaCoq.Template.utils.wGraph]
E:191 [binder, in MetaCoq.Translations.MiniHoTT_paths]
e:194 [binder, in MetaCoq.Template.utils.wGraph]
e:196 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
E:198 [binder, in MetaCoq.Template.common.uGraph]
e:201 [binder, in MetaCoq.Template.common.uGraph]
e:202 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
e:205 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
e:206 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
e:207 [binder, in MetaCoq.Translations.times_bool_fun]
e:207 [binder, in MetaCoq.Erasure.EWcbvEval]
e:209 [binder, in MetaCoq.Erasure.EWcbvEval]
E:21 [binder, in MetaCoq.Translations.param_binary]
e:211 [binder, in MetaCoq.Template.common.uGraph]
e:212 [binder, in MetaCoq.SafeChecker.PCUICErrors]
E:214 [binder, in MetaCoq.Template.common.uGraph]
e:216 [binder, in MetaCoq.Translations.times_bool_fun]
e:216 [binder, in MetaCoq.SafeChecker.PCUICErrors]
E:217 [binder, in MetaCoq.Template.common.uGraph]
e:223 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
e:228 [binder, in MetaCoq.Template.utils.wGraph]
e:236 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
E:238 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
E:24 [binder, in MetaCoq.Translations.param_generous_packed]
e:240 [binder, in MetaCoq.SafeChecker.PCUICErrors]
e:243 [binder, in MetaCoq.Template.utils.wGraph]
e:245 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
e:246 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
e:247 [binder, in MetaCoq.SafeChecker.PCUICErrors]
e:248 [binder, in MetaCoq.SafeChecker.PCUICErrors]
e:25 [binder, in MetaCoq.Translations.translation_utils]
E:25 [binder, in MetaCoq.Translations.param_cheap_packed]
e:250 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
e:251 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
e:254 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
e:256 [binder, in MetaCoq.SafeChecker.PCUICErrors]
e:261 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
e:263 [binder, in MetaCoq.Template.Universes]
e:264 [binder, in MetaCoq.Template.Universes]
e:265 [binder, in MetaCoq.SafeChecker.PCUICErrors]
e:270 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
e:274 [binder, in MetaCoq.Template.common.uGraph]
e:277 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
e:282 [binder, in MetaCoq.Template.Universes]
e:285 [binder, in MetaCoq.Erasure.EWcbvEval]
e:286 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
e:287 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
e:289 [binder, in MetaCoq.Template.common.uGraph]
e:292 [binder, in MetaCoq.Template.WcbvEval]
e:293 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
e:298 [binder, in MetaCoq.Template.WcbvEval]
E:30 [binder, in MetaCoq.Translations.translation_utils]
e:300 [binder, in MetaCoq.Template.utils.wGraph]
e:301 [binder, in MetaCoq.Erasure.EWcbvEval]
e:302 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
e:304 [binder, in MetaCoq.Erasure.EWcbvEval]
e:306 [binder, in MetaCoq.Template.utils.wGraph]
e:309 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
e:31 [binder, in MetaCoq.SafeChecker.PCUICErrors]
e:31 [binder, in MetaCoq.Erasure.EEtaExpanded]
E:31 [binder, in MetaCoq.Translations.param_generous_packed]
e:318 [binder, in MetaCoq.Template.utils.wGraph]
e:322 [binder, in MetaCoq.Template.common.uGraph]
e:327 [binder, in MetaCoq.Template.common.uGraph]
e:33 [binder, in MetaCoq.Template.Checker]
e:34 [binder, in MetaCoq.PCUIC.utils.PCUICUtils]
e:342 [binder, in MetaCoq.Template.common.uGraph]
e:346 [binder, in MetaCoq.Template.common.uGraph]
e:35 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
e:367 [binder, in MetaCoq.Template.common.uGraph]
e:379 [binder, in MetaCoq.Template.Checker]
e:380 [binder, in MetaCoq.Template.Checker]
e:386 [binder, in MetaCoq.Template.Checker]
e:39 [binder, in MetaCoq.Template.EnvMap]
e:411 [binder, in MetaCoq.Erasure.EWcbvEval]
e:412 [binder, in MetaCoq.Template.common.uGraph]
e:414 [binder, in MetaCoq.Template.common.uGraph]
e:419 [binder, in MetaCoq.Erasure.EWcbvEval]
e:421 [binder, in MetaCoq.Template.common.uGraph]
e:422 [binder, in MetaCoq.Template.common.uGraph]
e:423 [binder, in MetaCoq.Template.common.uGraph]
e:426 [binder, in MetaCoq.Template.utils.wGraph]
e:428 [binder, in MetaCoq.Template.utils.wGraph]
e:45 [binder, in MetaCoq.Template.EnvMap]
e:451 [binder, in MetaCoq.Erasure.EWcbvEval]
e:459 [binder, in MetaCoq.Erasure.EWcbvEval]
E:47 [binder, in MetaCoq.Translations.param_original]
e:477 [binder, in MetaCoq.Template.utils.wGraph]
e:479 [binder, in MetaCoq.Template.common.uGraph]
e:48 [binder, in MetaCoq.Template.Checker]
e:483 [binder, in MetaCoq.Template.common.uGraph]
e:49 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
e:491 [binder, in MetaCoq.Erasure.ErasureFunction]
e:497 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
e:497 [binder, in MetaCoq.Erasure.ErasureFunction]
e:5 [binder, in MetaCoq.Template.utils.MCEquality]
e:503 [binder, in MetaCoq.Erasure.ErasureFunction]
e:508 [binder, in MetaCoq.Erasure.ErasureFunction]
E:51 [binder, in MetaCoq.Translations.param_binary]
e:51 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
e:513 [binder, in MetaCoq.Erasure.ErasureFunction]
e:518 [binder, in MetaCoq.Erasure.ErasureFunction]
E:52 [binder, in MetaCoq.Translations.param_original]
e:524 [binder, in MetaCoq.Erasure.ErasureFunction]
e:530 [binder, in MetaCoq.Erasure.ErasureFunction]
e:535 [binder, in MetaCoq.Erasure.ErasureFunction]
e:540 [binder, in MetaCoq.Erasure.ErasureFunction]
e:543 [binder, in MetaCoq.Template.common.uGraph]
E:55 [binder, in MetaCoq.Template.utils.ReflectEq]
e:556 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
e:558 [binder, in MetaCoq.Erasure.ErasureFunction]
E:56 [binder, in MetaCoq.Translations.param_binary]
E:56 [binder, in MetaCoq.Translations.param_original]
e:562 [binder, in MetaCoq.Erasure.ErasureFunction]
e:567 [binder, in MetaCoq.Erasure.ErasureFunction]
e:5685 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
e:571 [binder, in MetaCoq.Erasure.ErasureFunction]
e:5712 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
e:575 [binder, in MetaCoq.Erasure.ErasureFunction]
e:579 [binder, in MetaCoq.Erasure.ErasureFunction]
e:58 [binder, in MetaCoq.Template.EnvMap]
e:583 [binder, in MetaCoq.Erasure.ErasureFunction]
e:588 [binder, in MetaCoq.Erasure.ErasureFunction]
E:59 [binder, in MetaCoq.Translations.param_original]
e:592 [binder, in MetaCoq.Erasure.ErasureFunction]
e:595 [binder, in MetaCoq.Template.utils.wGraph]
e:596 [binder, in MetaCoq.Erasure.ErasureFunction]
e:599 [binder, in MetaCoq.Template.common.uGraph]
E:6 [binder, in MetaCoq.Translations.translation_utils]
e:6 [binder, in MetaCoq.Erasure.ESpineView]
E:60 [binder, in MetaCoq.Translations.param_binary]
e:603 [binder, in MetaCoq.Template.common.uGraph]
e:607 [binder, in MetaCoq.Erasure.ErasureFunction]
e:608 [binder, in MetaCoq.Template.common.uGraph]
E:61 [binder, in MetaCoq.Translations.param_cheap_packed]
E:61 [binder, in MetaCoq.Translations.param_original]
e:611 [binder, in MetaCoq.Erasure.ErasureFunction]
e:616 [binder, in MetaCoq.Erasure.ErasureFunction]
e:62 [binder, in MetaCoq.Template.EnvMap]
e:622 [binder, in MetaCoq.Erasure.ErasureFunction]
e:628 [binder, in MetaCoq.Erasure.ErasureFunction]
E:63 [binder, in MetaCoq.Translations.param_binary]
e:630 [binder, in MetaCoq.Template.common.uGraph]
e:634 [binder, in MetaCoq.Erasure.ErasureFunction]
e:636 [binder, in MetaCoq.Template.common.uGraph]
e:638 [binder, in MetaCoq.Erasure.ErasureFunction]
e:643 [binder, in MetaCoq.Erasure.ErasureFunction]
e:649 [binder, in MetaCoq.Erasure.ErasureFunction]
E:65 [binder, in MetaCoq.Translations.param_binary]
e:655 [binder, in MetaCoq.Erasure.ErasureFunction]
e:66 [binder, in MetaCoq.Template.Universes]
e:67 [binder, in MetaCoq.Template.Universes]
e:68 [binder, in MetaCoq.Template.Universes]
e:68 [binder, in MetaCoq.Template.EnvMap]
E:69 [binder, in MetaCoq.Translations.param_generous_packed]
E:7 [binder, in MetaCoq.Translations.param_original]
E:70 [binder, in MetaCoq.Template.monad_utils]
e:70 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
e:71 [binder, in MetaCoq.Template.Universes]
e:718 [binder, in MetaCoq.Erasure.ErasureFunction]
e:72 [binder, in MetaCoq.Template.Universes]
e:720 [binder, in MetaCoq.Template.Universes]
e:722 [binder, in MetaCoq.Template.utils.wGraph]
e:723 [binder, in MetaCoq.Template.utils.wGraph]
e:724 [binder, in MetaCoq.Template.Universes]
e:724 [binder, in MetaCoq.Erasure.ErasureFunction]
e:728 [binder, in MetaCoq.Template.utils.wGraph]
e:730 [binder, in MetaCoq.Erasure.ErasureFunction]
e:734 [binder, in MetaCoq.Template.utils.wGraph]
e:735 [binder, in MetaCoq.Erasure.ErasureFunction]
e:739 [binder, in MetaCoq.Template.Universes]
e:74 [binder, in MetaCoq.Translations.translation_utils]
e:740 [binder, in MetaCoq.Template.utils.wGraph]
e:740 [binder, in MetaCoq.Erasure.ErasureFunction]
e:745 [binder, in MetaCoq.Erasure.ErasureFunction]
e:745 [binder, in MetaCoq.Translations.MiniHoTT]
e:747 [binder, in MetaCoq.Template.Universes]
e:751 [binder, in MetaCoq.Erasure.ErasureFunction]
e:752 [binder, in MetaCoq.Template.Universes]
e:753 [binder, in MetaCoq.Translations.MiniHoTT_paths]
e:757 [binder, in MetaCoq.Erasure.ErasureFunction]
e:76 [binder, in MetaCoq.Template.monad_utils]
e:762 [binder, in MetaCoq.Erasure.ErasureFunction]
e:765 [binder, in MetaCoq.Translations.MiniHoTT]
e:767 [binder, in MetaCoq.Erasure.ErasureFunction]
e:77 [binder, in MetaCoq.PCUIC.utils.PCUICUtils]
e:773 [binder, in MetaCoq.Translations.MiniHoTT_paths]
e:78 [binder, in MetaCoq.Template.TermEquality]
e:780 [binder, in MetaCoq.Template.utils.wGraph]
e:783 [binder, in MetaCoq.Template.utils.wGraph]
e:790 [binder, in MetaCoq.Template.utils.wGraph]
E:8 [binder, in MetaCoq.Template.monad_utils]
e:80 [binder, in MetaCoq.Translations.times_bool_fun2]
e:816 [binder, in MetaCoq.Template.utils.wGraph]
e:82 [binder, in MetaCoq.PCUIC.utils.PCUICUtils]
E:83 [binder, in MetaCoq.Translations.param_cheap_packed]
e:85 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
e:86 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
e:888 [binder, in MetaCoq.Template.utils.wGraph]
E:89 [binder, in MetaCoq.Translations.param_cheap_packed]
e:89 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
e:895 [binder, in MetaCoq.Template.utils.wGraph]
e:9 [binder, in MetaCoq.Template.EnvMap]
e:90 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
e:91 [binder, in MetaCoq.PCUIC.utils.PCUICUtils]
e:917 [binder, in MetaCoq.Template.utils.wGraph]
e:925 [binder, in MetaCoq.Template.utils.wGraph]
e:934 [binder, in MetaCoq.Template.utils.wGraph]
e:942 [binder, in MetaCoq.Template.utils.wGraph]
e:97 [binder, in MetaCoq.PCUIC.utils.PCUICUtils]
e:992 [binder, in MetaCoq.Template.utils.wGraph]
| 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) |