| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (19204 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (228 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (298 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1273 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (313 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (8163 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1514 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (52 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (352 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (534 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (727 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (402 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (333 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4833 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (182 entries) |
E
E [module, in MetaRocq.Erasure.Typed.ErasureCorrectness]E [module, in MetaRocq.Erasure.Typed.ExtractionCorrectness]
E [module, in MetaRocq.Erasure.Extract]
EArities [library]
EAst [library]
EAstUtils [library]
EBeta [library]
ecofix_subst_nth [lemma, in MetaRocq.Erasure.Prelim]
ECoInductiveToInductive [library]
EConstructorsAsBlocks [library]
ECorrect [section, in MetaRocq.Erasure.Typed.ErasureCorrectness]
ECorrect.no [variable, in MetaRocq.Erasure.Typed.ErasureCorrectness]
ECorrect.normalising_in [variable, in MetaRocq.Erasure.Typed.ErasureCorrectness]
ECorrect.X [variable, in MetaRocq.Erasure.Typed.ErasureCorrectness]
ECorrect.X_type [variable, in MetaRocq.Erasure.Typed.ErasureCorrectness]
ECSubst [library]
Edecompose_app_annot [definition, in MetaRocq.Erasure.Typed.Annotations]
Edecompose_lam_annot [definition, in MetaRocq.Erasure.Typed.Annotations]
EDeps [library]
EdgeSet_triple [definition, in MetaRocq.Common.uGraph]
EdgeSet_pair [definition, in MetaRocq.Common.uGraph]
edge_of_constraint [definition, in MetaRocq.Common.uGraph]
edge_of_level [definition, in MetaRocq.Common.uGraph]
EEnvCorrect [section, in MetaRocq.Erasure.Typed.ErasureCorrectness]
EEnvCorrect.normalising_in [variable, in MetaRocq.Erasure.Typed.ErasureCorrectness]
EEnvCorrect.X [variable, in MetaRocq.Erasure.Typed.ErasureCorrectness]
EEnvCorrect.X_type [variable, in MetaRocq.Erasure.Typed.ErasureCorrectness]
EEnvFlags [section, in MetaRocq.Erasure.EExtends]
EEnvFlags [section, in MetaRocq.Erasure.EWellformed]
EEnvFlags [record, in MetaRocq.Erasure.EWellformed]
EEnvFlags.efl [variable, in MetaRocq.Erasure.EExtends]
EEnvFlags.efl [variable, in MetaRocq.Erasure.EWellformed]
EEnvFlags.Σ [variable, in MetaRocq.Erasure.EWellformed]
EEnvMap [library]
EEtaExpanded [library]
EEtaExpandedFix [library]
EExtends [library]
efix_subst_nth [lemma, in MetaRocq.Erasure.Prelim]
EGenericGlobalMap [library]
EGenericMapEnv [library]
EGlobalEnv [library]
EGlobalFragment [library]
EImplementBox [library]
EInduction [library]
einfering_sort_isType [lemma, in MetaRocq.PCUIC.Bidirectional.BDToPCUIC]
EInlineProjections [library]
EInlining [library]
ELiftSubst [library]
elim [section, in MetaRocq.Erasure.ErasureFunctionProperties]
elimP [lemma, in MetaRocq.Utils.ReflectEq]
elimT [lemma, in MetaRocq.Utils.MRReflect]
elim_restriction_works_proj [lemma, in MetaRocq.PCUIC.PCUICElimination]
elim_restriction_works_proj_kelim1 [lemma, in MetaRocq.PCUIC.PCUICElimination]
elim_restriction_works [lemma, in MetaRocq.PCUIC.PCUICElimination]
elim_restriction_works_kelim [lemma, in MetaRocq.PCUIC.PCUICElimination]
elim_sort_intype [lemma, in MetaRocq.PCUIC.PCUICElimination]
elim_restriction_works_kelim1 [lemma, in MetaRocq.PCUIC.PCUICElimination]
elim_inspect [lemma, in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
Elim' [section, in MetaRocq.Erasure.EArities]
Elim'.cf [variable, in MetaRocq.Erasure.EArities]
Elim'.Hcf [variable, in MetaRocq.Erasure.EArities]
Elim'.wfΣ [variable, in MetaRocq.Erasure.EArities]
Elim'.Σ [variable, in MetaRocq.Erasure.EArities]
elim.ih [variable, in MetaRocq.Erasure.ErasureFunctionProperties]
elim.P [variable, in MetaRocq.Erasure.ErasureFunctionProperties]
elim.Σ [variable, in MetaRocq.Erasure.ErasureFunctionProperties]
elookup_env_cons_disc [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
elookup_env_cons_fresh [lemma, in MetaRocq.Erasure.EGlobalEnv]
emax [definition, in MetaRocq.Common.BasicAst]
emkApps_snoc [lemma, in MetaRocq.Erasure.Prelim]
emptys [constructor, in MetaRocq.PCUIC.PCUICSubstitution]
emptyslet [constructor, in MetaRocq.PCUIC.PCUICSubstitution]
empty_contextset_subset [lemma, in MetaRocq.Common.Universes]
empty_trans_env [definition, in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
Empty_set_FinitelyListablePackage [instance, in MetaRocq.Utils.MRListable]
empty_ext [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
enable_typed_erasure [projection, in MetaRocq.ErasurePlugin.Erasure]
enable_unsafe [projection, in MetaRocq.ErasurePlugin.Erasure]
enumerate_unique [lemma, in MetaRocq.Utils.MRListable]
enumerate_smallb [projection, in MetaRocq.Utils.MRListable]
Env [module, in MetaRocq.Template.Ast]
EnvCheck [inductive, in MetaRocq.SafeChecker.PCUICErrors]
EnvCheck [section, in MetaRocq.SafeChecker.PCUICErrors]
EnvCheck [inductive, in MetaRocq.Template.Checker]
envcheck_monad_exc [instance, in MetaRocq.SafeChecker.PCUICErrors]
envcheck_monad [instance, in MetaRocq.SafeChecker.PCUICErrors]
EnvCheck_sind [definition, in MetaRocq.SafeChecker.PCUICErrors]
EnvCheck_rec [definition, in MetaRocq.SafeChecker.PCUICErrors]
EnvCheck_ind [definition, in MetaRocq.SafeChecker.PCUICErrors]
EnvCheck_rect [definition, in MetaRocq.SafeChecker.PCUICErrors]
EnvCheck_wf_env_ext [definition, in MetaRocq.SafeCheckerPlugin.SafeTemplateChecker]
EnvCheck_X_env_ext_type [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
envcheck_monad [instance, in MetaRocq.Template.Checker]
EnvCheck_sind [definition, in MetaRocq.Template.Checker]
EnvCheck_rec [definition, in MetaRocq.Template.Checker]
EnvCheck_ind [definition, in MetaRocq.Template.Checker]
EnvCheck_rect [definition, in MetaRocq.Template.Checker]
EnvCheck.abstract_structure [variable, in MetaRocq.SafeChecker.PCUICErrors]
EnvDecide [module, in MetaRocq.Template.ReflectAst]
EnvDecide.constant_body_eq_dec [instance, in MetaRocq.Template.ReflectAst]
EnvDecide.constructor_body_eq_dec [instance, in MetaRocq.Template.ReflectAst]
EnvDecide.context_eq_dec [instance, in MetaRocq.Template.ReflectAst]
EnvDecide.global_decl_eq_dec [instance, in MetaRocq.Template.ReflectAst]
EnvDecide.mutual_inductive_body_eq_dec [instance, in MetaRocq.Template.ReflectAst]
EnvDecide.one_inductive_body_eq_dec [instance, in MetaRocq.Template.ReflectAst]
EnvDecide.projection_body_eq_dec [instance, in MetaRocq.Template.ReflectAst]
EnvError [constructor, in MetaRocq.SafeChecker.PCUICErrors]
EnvError [constructor, in MetaRocq.Template.Checker]
Environment [module, in MetaRocq.Common.Environment]
environment [definition, in MetaRocq.Erasure.EWcbvEvalNamed]
Environment [library]
EnvironmentDecide [module, in MetaRocq.Common.Environment]
EnvironmentDecideReflectInstances [module, in MetaRocq.Common.Environment]
EnvironmentDecide.constant_body_eq_dec [instance, in MetaRocq.Common.Environment]
EnvironmentDecide.constructor_body_eq_dec [instance, in MetaRocq.Common.Environment]
EnvironmentDecide.context_eq_dec [instance, in MetaRocq.Common.Environment]
EnvironmentDecide.global_decl_eq_dec [instance, in MetaRocq.Common.Environment]
EnvironmentDecide.mutual_inductive_body_eq_dec [instance, in MetaRocq.Common.Environment]
EnvironmentDecide.one_inductive_body_eq_dec [instance, in MetaRocq.Common.Environment]
EnvironmentDecide.projection_body_eq_dec [instance, in MetaRocq.Common.Environment]
EnvironmentReflect [module, in MetaRocq.Common.EnvironmentReflect]
EnvironmentReflect [library]
EnvironmentReflectSig [module, in MetaRocq.Common.EnvironmentReflect]
EnvironmentReflect.compatibleb [definition, in MetaRocq.Common.EnvironmentReflect]
EnvironmentReflect.compatibleP [lemma, in MetaRocq.Common.EnvironmentReflect]
EnvironmentReflect.compatible_spec [lemma, in MetaRocq.Common.EnvironmentReflect]
EnvironmentReflect.compatible_globals_spec [lemma, in MetaRocq.Common.EnvironmentReflect]
EnvironmentReflect.compatible_globalsP [lemma, in MetaRocq.Common.EnvironmentReflect]
EnvironmentReflect.compatible_globalsb [definition, in MetaRocq.Common.EnvironmentReflect]
EnvironmentReflect.extendsb [definition, in MetaRocq.Common.EnvironmentReflect]
EnvironmentReflect.extendsb_decls_part [abbreviation, in MetaRocq.Common.EnvironmentReflect]
EnvironmentReflect.extendsT [lemma, in MetaRocq.Common.EnvironmentReflect]
EnvironmentReflect.extends_strictly_on_decls_spec [lemma, in MetaRocq.Common.EnvironmentReflect]
EnvironmentReflect.extends_decls_spec [lemma, in MetaRocq.Common.EnvironmentReflect]
EnvironmentReflect.extends_spec [lemma, in MetaRocq.Common.EnvironmentReflect]
EnvironmentReflect.extends_strictly_on_declsT [lemma, in MetaRocq.Common.EnvironmentReflect]
EnvironmentReflect.extends_declsT [lemma, in MetaRocq.Common.EnvironmentReflect]
EnvironmentReflect.extends_strictly_on_declsb [definition, in MetaRocq.Common.EnvironmentReflect]
EnvironmentReflect.extends_declsb [definition, in MetaRocq.Common.EnvironmentReflect]
EnvironmentReflect.extends_decls_partT [lemma, in MetaRocq.Common.EnvironmentReflect]
EnvironmentReflect.strictly_extends_decls_spec [lemma, in MetaRocq.Common.EnvironmentReflect]
EnvironmentReflect.strictly_extends_declsT [lemma, in MetaRocq.Common.EnvironmentReflect]
EnvironmentReflect.strictly_extends_declsb [definition, in MetaRocq.Common.EnvironmentReflect]
EnvironmentReflect.strictly_extends_decls_partT [lemma, in MetaRocq.Common.EnvironmentReflect]
EnvironmentReflect.strictly_extendsb_decls_part [abbreviation, in MetaRocq.Common.EnvironmentReflect]
EnvironmentSig [module, in MetaRocq.Common.Environment]
EnvironmentTyping [library]
Environment.add_global_decl [definition, in MetaRocq.Common.Environment]
Environment.All_decls_to_alpha [lemma, in MetaRocq.Common.Environment]
Environment.All_decls_alpha_impl [lemma, in MetaRocq.Common.Environment]
Environment.All_decls_impl [lemma, in MetaRocq.Common.Environment]
Environment.All_decls_alpha_sind [definition, in MetaRocq.Common.Environment]
Environment.All_decls_alpha_rec [definition, in MetaRocq.Common.Environment]
Environment.All_decls_alpha_ind [definition, in MetaRocq.Common.Environment]
Environment.All_decls_alpha_rect [definition, in MetaRocq.Common.Environment]
Environment.All_decls_alpha [inductive, in MetaRocq.Common.Environment]
Environment.All_decls_sind [definition, in MetaRocq.Common.Environment]
Environment.All_decls_rec [definition, in MetaRocq.Common.Environment]
Environment.All_decls_ind [definition, in MetaRocq.Common.Environment]
Environment.All_decls_rect [definition, in MetaRocq.Common.Environment]
Environment.All_decls [inductive, in MetaRocq.Common.Environment]
Environment.All2_fold_over [definition, in MetaRocq.Common.Environment]
Environment.arities_context_length [lemma, in MetaRocq.Common.Environment]
Environment.arities_context [definition, in MetaRocq.Common.Environment]
Environment.array_uctx [definition, in MetaRocq.Common.Environment]
Environment.compatible [definition, in MetaRocq.Common.Environment]
Environment.compatible_globals [definition, in MetaRocq.Common.Environment]
Environment.ConstantDecl [constructor, in MetaRocq.Common.Environment]
Environment.constant_body [record, in MetaRocq.Common.Environment]
Environment.constructor_body [record, in MetaRocq.Common.Environment]
Environment.context [definition, in MetaRocq.Common.Environment]
Environment.context_assumptions_lift_context [lemma, in MetaRocq.Common.Environment]
Environment.context_assumptions_subst_context [lemma, in MetaRocq.Common.Environment]
Environment.context_assumptions_subst_instance [lemma, in MetaRocq.Common.Environment]
Environment.context_assumptions_mapi [lemma, in MetaRocq.Common.Environment]
Environment.context_assumptions_rev [lemma, in MetaRocq.Common.Environment]
Environment.context_assumptions_app [lemma, in MetaRocq.Common.Environment]
Environment.context_assumptions_map [lemma, in MetaRocq.Common.Environment]
Environment.context_assumptions_length_bound [lemma, in MetaRocq.Common.Environment]
Environment.context_assumptions_fold [lemma, in MetaRocq.Common.Environment]
Environment.context_assumptions [definition, in MetaRocq.Common.Environment]
Environment.context_decl [abbreviation, in MetaRocq.Common.Environment]
Environment.cstr_arity [projection, in MetaRocq.Common.Environment]
Environment.cstr_type [projection, in MetaRocq.Common.Environment]
Environment.cstr_indices [projection, in MetaRocq.Common.Environment]
Environment.cstr_args [projection, in MetaRocq.Common.Environment]
Environment.cstr_name [projection, in MetaRocq.Common.Environment]
Environment.cst_relevance [projection, in MetaRocq.Common.Environment]
Environment.cst_universes [projection, in MetaRocq.Common.Environment]
Environment.cst_body [projection, in MetaRocq.Common.Environment]
Environment.cst_type [projection, in MetaRocq.Common.Environment]
Environment.declarations [projection, in MetaRocq.Common.Environment]
Environment.declared_kername_set_mem_iff [lemma, in MetaRocq.Common.Environment]
Environment.declared_kername_set_spec [lemma, in MetaRocq.Common.Environment]
Environment.declared_kername_set [definition, in MetaRocq.Common.Environment]
Environment.empty_ext [definition, in MetaRocq.Common.Environment]
Environment.empty_global_env [definition, in MetaRocq.Common.Environment]
Environment.eta_global_env [lemma, in MetaRocq.Common.Environment]
Environment.expand_lets_ctx_length [lemma, in MetaRocq.Common.Environment]
Environment.expand_lets_k_ctx_length [lemma, in MetaRocq.Common.Environment]
Environment.expand_lets_ctx [definition, in MetaRocq.Common.Environment]
Environment.expand_lets_k_ctx [definition, in MetaRocq.Common.Environment]
Environment.expand_lets [definition, in MetaRocq.Common.Environment]
Environment.expand_lets_k [definition, in MetaRocq.Common.Environment]
Environment.extended_subst_length [lemma, in MetaRocq.Common.Environment]
Environment.extended_subst [definition, in MetaRocq.Common.Environment]
Environment.extends [definition, in MetaRocq.Common.Environment]
Environment.extends_r_merge [lemma, in MetaRocq.Common.Environment]
Environment.extends_r_merge_globals [lemma, in MetaRocq.Common.Environment]
Environment.extends_l_merge [lemma, in MetaRocq.Common.Environment]
Environment.extends_strictly_on_decls_l_merge [lemma, in MetaRocq.Common.Environment]
Environment.extends_l_merge_globals [lemma, in MetaRocq.Common.Environment]
Environment.extends_trans [instance, in MetaRocq.Common.Environment]
Environment.extends_strictly_on_decls_trans [instance, in MetaRocq.Common.Environment]
Environment.extends_decls_trans [instance, in MetaRocq.Common.Environment]
Environment.extends_decls_part_trans [lemma, in MetaRocq.Common.Environment]
Environment.extends_decls_part_globals_trans [lemma, in MetaRocq.Common.Environment]
Environment.extends_decls_part_refl [lemma, in MetaRocq.Common.Environment]
Environment.extends_decls_part_globals_refl [lemma, in MetaRocq.Common.Environment]
Environment.extends_refl [lemma, in MetaRocq.Common.Environment]
Environment.extends_strictly_on_decls_refl [lemma, in MetaRocq.Common.Environment]
Environment.extends_decls_refl [instance, in MetaRocq.Common.Environment]
Environment.extends_strictly_on_decls_extends_subrel [instance, in MetaRocq.Common.Environment]
Environment.extends_decls_extends_subrel [instance, in MetaRocq.Common.Environment]
Environment.extends_strictly_on_decls_extends [instance, in MetaRocq.Common.Environment]
Environment.extends_decls_extends [instance, in MetaRocq.Common.Environment]
Environment.extends_strictly_on_decls [definition, in MetaRocq.Common.Environment]
Environment.extends_decls [definition, in MetaRocq.Common.Environment]
Environment.extends_decls_part [abbreviation, in MetaRocq.Common.Environment]
Environment.extends_decls_part_globals [abbreviation, in MetaRocq.Common.Environment]
Environment.fix_context [definition, in MetaRocq.Common.Environment]
Environment.fst_ctx [definition, in MetaRocq.Common.Environment]
Environment.global_env_ext [definition, in MetaRocq.Common.Environment]
Environment.global_env [record, in MetaRocq.Common.Environment]
Environment.global_declarations [definition, in MetaRocq.Common.Environment]
Environment.global_decl_sind [definition, in MetaRocq.Common.Environment]
Environment.global_decl_rec [definition, in MetaRocq.Common.Environment]
Environment.global_decl_ind [definition, in MetaRocq.Common.Environment]
Environment.global_decl_rect [definition, in MetaRocq.Common.Environment]
Environment.global_decl [inductive, in MetaRocq.Common.Environment]
Environment.hd_error_lookup_globals [lemma, in MetaRocq.Common.Environment]
Environment.InductiveDecl [constructor, in MetaRocq.Common.Environment]
Environment.ind_projs_map [lemma, in MetaRocq.Common.Environment]
Environment.ind_pars_map [lemma, in MetaRocq.Common.Environment]
Environment.ind_ctors_map [lemma, in MetaRocq.Common.Environment]
Environment.ind_type_map [lemma, in MetaRocq.Common.Environment]
Environment.ind_variance [projection, in MetaRocq.Common.Environment]
Environment.ind_universes [projection, in MetaRocq.Common.Environment]
Environment.ind_bodies [projection, in MetaRocq.Common.Environment]
Environment.ind_params [projection, in MetaRocq.Common.Environment]
Environment.ind_npars [projection, in MetaRocq.Common.Environment]
Environment.ind_finite [projection, in MetaRocq.Common.Environment]
Environment.ind_relevance [projection, in MetaRocq.Common.Environment]
Environment.ind_projs [projection, in MetaRocq.Common.Environment]
Environment.ind_ctors [projection, in MetaRocq.Common.Environment]
Environment.ind_kelim [projection, in MetaRocq.Common.Environment]
Environment.ind_type [projection, in MetaRocq.Common.Environment]
Environment.ind_sort [projection, in MetaRocq.Common.Environment]
Environment.ind_indices [projection, in MetaRocq.Common.Environment]
Environment.ind_name [projection, in MetaRocq.Common.Environment]
Environment.is_assumption_context [definition, in MetaRocq.Common.Environment]
Environment.it_mkProd_or_LetIn_app [lemma, in MetaRocq.Common.Environment]
Environment.it_mkProd_or_LetIn [definition, in MetaRocq.Common.Environment]
Environment.it_mkLambda_or_LetIn [definition, in MetaRocq.Common.Environment]
Environment.judgment [definition, in MetaRocq.Common.Environment]
Environment.lift_context_length [lemma, in MetaRocq.Common.Environment]
Environment.lift_context_alt [lemma, in MetaRocq.Common.Environment]
Environment.lift_context [definition, in MetaRocq.Common.Environment]
Environment.lift_decl [definition, in MetaRocq.Common.Environment]
Environment.lookup_globals_filter [lemma, in MetaRocq.Common.Environment]
Environment.lookup_globals_app [lemma, in MetaRocq.Common.Environment]
Environment.lookup_env_extends_NoDup [lemma, in MetaRocq.Common.Environment]
Environment.lookup_global_extends_NoDup [lemma, in MetaRocq.Common.Environment]
Environment.lookup_global_Some_iff_In_NoDup [lemma, in MetaRocq.Common.Environment]
Environment.lookup_global_Some_if_In [lemma, in MetaRocq.Common.Environment]
Environment.lookup_globals_In [lemma, in MetaRocq.Common.Environment]
Environment.lookup_globals_nil [lemma, in MetaRocq.Common.Environment]
Environment.lookup_global_None [lemma, in MetaRocq.Common.Environment]
Environment.lookup_envs [definition, in MetaRocq.Common.Environment]
Environment.lookup_globals [definition, in MetaRocq.Common.Environment]
Environment.lookup_env [definition, in MetaRocq.Common.Environment]
Environment.lookup_global [definition, in MetaRocq.Common.Environment]
Environment.map_mutual_inductive_body [definition, in MetaRocq.Common.Environment]
Environment.map_cst_body [lemma, in MetaRocq.Common.Environment]
Environment.map_cst_type [lemma, in MetaRocq.Common.Environment]
Environment.map_constant_body [definition, in MetaRocq.Common.Environment]
Environment.map_one_inductive_body [definition, in MetaRocq.Common.Environment]
Environment.map_projection_body [definition, in MetaRocq.Common.Environment]
Environment.map_constructor_body [definition, in MetaRocq.Common.Environment]
Environment.merge_global_envs [definition, in MetaRocq.Common.Environment]
Environment.merge_globals [definition, in MetaRocq.Common.Environment]
Environment.mkLambda_or_LetIn [definition, in MetaRocq.Common.Environment]
Environment.mkProd_or_LetIn [definition, in MetaRocq.Common.Environment]
Environment.mutual_inductive_body [record, in MetaRocq.Common.Environment]
Environment.NoDup_lookup_globals_eq [lemma, in MetaRocq.Common.Environment]
Environment.NoDup_length_lookup_globals [lemma, in MetaRocq.Common.Environment]
Environment.nth_error_lt [lemma, in MetaRocq.Common.Environment]
Environment.nth_error_ge [lemma, in MetaRocq.Common.Environment]
Environment.nth_error_fold_context_k_eq [lemma, in MetaRocq.Common.Environment]
Environment.nth_error_fold_context_k [lemma, in MetaRocq.Common.Environment]
Environment.one_inductive_body [record, in MetaRocq.Common.Environment]
Environment.on_contexts_over [abbreviation, in MetaRocq.Common.Environment]
Environment.on_contexts [abbreviation, in MetaRocq.Common.Environment]
Environment.on_decls [abbreviation, in MetaRocq.Common.Environment]
Environment.on_vdef_alpha [constructor, in MetaRocq.Common.Environment]
Environment.on_vass_alpha [constructor, in MetaRocq.Common.Environment]
Environment.on_vdef [constructor, in MetaRocq.Common.Environment]
Environment.on_vass [constructor, in MetaRocq.Common.Environment]
Environment.primitive_invariants [definition, in MetaRocq.Common.Environment]
Environment.primitive_constant [definition, in MetaRocq.Common.Environment]
Environment.program [definition, in MetaRocq.Common.Environment]
Environment.projection_body [record, in MetaRocq.Common.Environment]
Environment.projs [definition, in MetaRocq.Common.Environment]
Environment.projs_length [lemma, in MetaRocq.Common.Environment]
Environment.proj_type [projection, in MetaRocq.Common.Environment]
Environment.proj_relevance [projection, in MetaRocq.Common.Environment]
Environment.proj_name [projection, in MetaRocq.Common.Environment]
Environment.reln [definition, in MetaRocq.Common.Environment]
Environment.reln_alt_eq [lemma, in MetaRocq.Common.Environment]
Environment.reln_alt [definition, in MetaRocq.Common.Environment]
Environment.reln_list_lift_above [lemma, in MetaRocq.Common.Environment]
Environment.reln_fold [lemma, in MetaRocq.Common.Environment]
Environment.retroknowledge [projection, in MetaRocq.Common.Environment]
Environment.set_declarations [definition, in MetaRocq.Common.Environment]
Environment.set_binder_name [definition, in MetaRocq.Common.Environment]
Environment.smash_context_app [lemma, in MetaRocq.Common.Environment]
Environment.smash_context_length [lemma, in MetaRocq.Common.Environment]
Environment.smash_context [definition, in MetaRocq.Common.Environment]
Environment.strictly_extends_decls_l_merge_globals [lemma, in MetaRocq.Common.Environment]
Environment.strictly_extends_decls_trans [instance, in MetaRocq.Common.Environment]
Environment.strictly_extends_decls_part_trans [lemma, in MetaRocq.Common.Environment]
Environment.strictly_extends_decls_part_globals_trans [lemma, in MetaRocq.Common.Environment]
Environment.strictly_extends_decls_part_refl [lemma, in MetaRocq.Common.Environment]
Environment.strictly_extends_decls_part_globals_refl [lemma, in MetaRocq.Common.Environment]
Environment.strictly_extends_decls_refl [instance, in MetaRocq.Common.Environment]
Environment.strictly_extends_decls_extends_subrel [instance, in MetaRocq.Common.Environment]
Environment.strictly_extends_decls_extends_strictly_on_decls_subrel [instance, in MetaRocq.Common.Environment]
Environment.strictly_extends_decls_extends_decls_subrel [instance, in MetaRocq.Common.Environment]
Environment.strictly_extends_decls_extends_strictly_on_decls [instance, in MetaRocq.Common.Environment]
Environment.strictly_extends_decls_extends_decls [instance, in MetaRocq.Common.Environment]
Environment.strictly_extends_decls_extends_part [lemma, in MetaRocq.Common.Environment]
Environment.strictly_extends_decls_extends_part_globals [lemma, in MetaRocq.Common.Environment]
Environment.strictly_extends_decls [definition, in MetaRocq.Common.Environment]
Environment.strictly_extends_decls_part [abbreviation, in MetaRocq.Common.Environment]
Environment.strictly_extends_decls_part_globals [abbreviation, in MetaRocq.Common.Environment]
Environment.subst_instance_length [lemma, in MetaRocq.Common.Environment]
Environment.subst_instance_context [instance, in MetaRocq.Common.Environment]
Environment.subst_instance_decl [instance, in MetaRocq.Common.Environment]
Environment.subst_telescope [definition, in MetaRocq.Common.Environment]
Environment.subst_context_snoc [lemma, in MetaRocq.Common.Environment]
Environment.subst_context_alt [lemma, in MetaRocq.Common.Environment]
Environment.subst_context_nil [lemma, in MetaRocq.Common.Environment]
Environment.subst_context_length [lemma, in MetaRocq.Common.Environment]
Environment.subst_decl [definition, in MetaRocq.Common.Environment]
Environment.subst_context [definition, in MetaRocq.Common.Environment]
Environment.tImpl [definition, in MetaRocq.Common.Environment]
Environment.to_extended_list_k_cons [lemma, in MetaRocq.Common.Environment]
Environment.to_extended_list_lift_above [lemma, in MetaRocq.Common.Environment]
Environment.to_extended_list_k_spec [lemma, in MetaRocq.Common.Environment]
Environment.to_extended_list [definition, in MetaRocq.Common.Environment]
Environment.to_extended_list_k [definition, in MetaRocq.Common.Environment]
Environment.universes [projection, in MetaRocq.Common.Environment]
Environment.vass [definition, in MetaRocq.Common.Environment]
Environment.vdef [definition, in MetaRocq.Common.Environment]
EnvMap [module, in MetaRocq.Common.EnvMap]
EnvMap [library]
EnvMap.add [definition, in MetaRocq.Common.EnvMap]
EnvMap.empty [definition, in MetaRocq.Common.EnvMap]
EnvMap.equal [definition, in MetaRocq.Common.EnvMap]
EnvMap.fold_left_cons [lemma, in MetaRocq.Common.EnvMap]
EnvMap.fresh_globals_iff_NoDup [lemma, in MetaRocq.Common.EnvMap]
EnvMap.fresh_global_iff_not_In [lemma, in MetaRocq.Common.EnvMap]
EnvMap.fresh_globals_sind [definition, in MetaRocq.Common.EnvMap]
EnvMap.fresh_globals_ind [definition, in MetaRocq.Common.EnvMap]
EnvMap.fresh_globals_cons [constructor, in MetaRocq.Common.EnvMap]
EnvMap.fresh_globals_empty [constructor, in MetaRocq.Common.EnvMap]
EnvMap.fresh_globals [inductive, in MetaRocq.Common.EnvMap]
EnvMap.fresh_global [definition, in MetaRocq.Common.EnvMap]
EnvMap.gso [lemma, in MetaRocq.Common.EnvMap]
EnvMap.gss [lemma, in MetaRocq.Common.EnvMap]
EnvMap.lookup [definition, in MetaRocq.Common.EnvMap]
EnvMap.lookup_spec [lemma, in MetaRocq.Common.EnvMap]
EnvMap.lookup_global [definition, in MetaRocq.Common.EnvMap]
EnvMap.lookup_add_other [lemma, in MetaRocq.Common.EnvMap]
EnvMap.lookup_add [lemma, in MetaRocq.Common.EnvMap]
EnvMap.of_global_env_cons [lemma, in MetaRocq.Common.EnvMap]
EnvMap.of_global_env [definition, in MetaRocq.Common.EnvMap]
EnvMap.Poly [section, in MetaRocq.Common.EnvMap]
EnvMap.Poly.A [variable, in MetaRocq.Common.EnvMap]
EnvMap.remove [definition, in MetaRocq.Common.EnvMap]
EnvMap.remove_add_o [lemma, in MetaRocq.Common.EnvMap]
EnvMap.remove_add_eq [lemma, in MetaRocq.Common.EnvMap]
EnvMap.repr [definition, in MetaRocq.Common.EnvMap]
EnvMap.repr_add [lemma, in MetaRocq.Common.EnvMap]
EnvMap.repr_global_env [lemma, in MetaRocq.Common.EnvMap]
EnvMap.t [definition, in MetaRocq.Common.EnvMap]
EnvMap.unfold_equal [lemma, in MetaRocq.Common.EnvMap]
EnvReflect [module, in MetaRocq.Template.ReflectAst]
EnvTyping [module, in MetaRocq.Common.EnvironmentTyping]
EnvTypingSig [module, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_rel_sorting_size [definition, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_sorting_size [definition, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_rel_size [definition, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_size [definition, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_size_app [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_rel_size_gen [abbreviation, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_size_pos [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_size_gen [definition, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_size.ssize [variable, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_size.csize [variable, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_size.sorting [variable, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_size.checking [variable, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_size [section, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_over_2 [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_over_sorting_2 [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_over [definition, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_over_sorting_sind [definition, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_over_sorting_rec [definition, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_over_sorting_ind [definition, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_over_sorting_rect [definition, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_over_sorting [inductive, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_lift_prod_inv [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_prod_inv [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_rel_app [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_app [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_rel_app_inv [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_app_inv [definition, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_app_rel [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_local_rel [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_rel_local [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_rel_ind1 [definition, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_rel_tip [definition, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_rel_def [definition, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_rel_abs [definition, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_rel_snoc [definition, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_rel_nil [definition, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_rel [definition, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_rel [section, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_cst [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_nth_error [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_app_skipn [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_skipn [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_impl_ind [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_impl [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_impl_gen [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_fold [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_map [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_ind1 [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_tip [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_snoc [definition, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_sind [definition, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_rec [definition, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_ind [definition, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_rect [definition, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env [inductive, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.Bidirectional [section, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.Bidirectional.checking [variable, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.Bidirectional.checking_size [variable, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.Bidirectional.sorting [variable, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.Bidirectional.sorting_size [variable, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.ctx_inst_impl [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.ctx_inst_impl_gen [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.ctx_inst_sind [definition, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.ctx_inst_rec [definition, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.ctx_inst_ind [definition, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.ctx_inst_rect [definition, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.ctx_inst_def [constructor, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.ctx_inst_ass [constructor, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.ctx_inst_nil [constructor, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.ctx_inst [inductive, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_typing_size_impl [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_sorting_size_impl [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_typing_size [abbreviation, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_sorting_size [abbreviation, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_sorting_size_gen_impl [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_sorting_size_gen [definition, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_sorting_size_gen.ssize [variable, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_sorting_size_gen.csize [variable, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_sorting_size_gen.sorting [variable, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_sorting_size_gen.checking [variable, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_sorting_size_gen [section, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_typing_impl [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_sorting_impl [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_typing_mapu [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_typing_map [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_typing_f_impl [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_sorting_f_impl [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_typing_fu_impl [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_sorting_fu_impl [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_sorting_it_impl [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_sorting_f_it_impl [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_sorting_fu_it_impl [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_sorting_it_impl_gen [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_sorting_ex_it_impl_gen [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_sorting_forget_body [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_sorting_forget_univ [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_sorting_extract [definition, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_wfbu_term_f_impl [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_wf_term_impl [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_wf_term_f_impl [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_wf_term_it_impl [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_typing_conj [definition, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_typing [abbreviation, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_typing1 [abbreviation, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_typing0 [definition, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_sorting2 [abbreviation, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_sorting1 [abbreviation, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_sorting [definition, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_wfbu_term [definition, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_wfb_term1 [abbreviation, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_wfb_term [definition, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_wfu_term [definition, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_wf_term1 [abbreviation, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_wf_term [definition, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.localenv_over_cons_def [constructor, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.localenv_over_cons_abs [constructor, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.localenv_over_nil [constructor, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.localenv_cons [definition, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.localenv_cons_def [constructor, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.localenv_cons_abs [constructor, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.localenv_nil [constructor, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.nth_error_All_local_env_over [lemma, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.on_def_body_size [abbreviation, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.on_def_body_sorting_size [abbreviation, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.on_def_type_size [abbreviation, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.on_def_type_sorting_size [abbreviation, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.on_def_body_size_gen [definition, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.on_def_type_size_gen [definition, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.on_wf_local_decl [definition, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.on_def_body [definition, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.on_def_type [definition, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.on_local_decl [abbreviation, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.option_default_size [definition, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.Prop_conj [abbreviation, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.Prop_local_conj [abbreviation, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.Regular [section, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.Regular.typing [variable, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.Regular.typing_size [variable, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.TypeCtxInst [section, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.TypeCtxInst.typing [variable, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.TypeLocal [section, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.TypeLocalOver [section, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.TypeLocalOver.checking [variable, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.TypeLocalOver.cproperty [variable, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.TypeLocalOver.sorting [variable, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.TypeLocalOver.sproperty [variable, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.TypeLocal.typing [variable, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.typing_sort_size1 [abbreviation, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.typing_sort_size [abbreviation, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.typing_sort2 [abbreviation, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.typing_sort1 [abbreviation, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.typing_sort [abbreviation, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.unlift_TypUniv [definition, in MetaRocq.Common.EnvironmentTyping]
EnvTyping.unlift_TermTyp [lemma, in MetaRocq.Common.EnvironmentTyping]
env_annots [definition, in MetaRocq.Erasure.Typed.Annotations]
env_prop_bd [definition, in MetaRocq.PCUIC.Bidirectional.BDTyping]
env_closed [definition, in MetaRocq.Erasure.Typed.ClosedAux]
env_prop_sigma [lemma, in MetaRocq.PCUIC.PCUICTyping]
env_prop_wf_local [lemma, in MetaRocq.PCUIC.PCUICTyping]
env_prop_typing [lemma, in MetaRocq.PCUIC.PCUICTyping]
env_prop [definition, in MetaRocq.PCUIC.PCUICTyping]
env_error_sind [definition, in MetaRocq.SafeChecker.PCUICErrors]
env_error_rec [definition, in MetaRocq.SafeChecker.PCUICErrors]
env_error_ind [definition, in MetaRocq.SafeChecker.PCUICErrors]
env_error_rect [definition, in MetaRocq.SafeChecker.PCUICErrors]
env_error [inductive, in MetaRocq.SafeChecker.PCUICErrors]
env_flags [definition, in MetaRocq.Erasure.EWcbvEvalEtaInd]
env_prop_sigma [lemma, in MetaRocq.Template.Typing]
env_prop_wf_local [lemma, in MetaRocq.Template.Typing]
env_prop_typing [lemma, in MetaRocq.Template.Typing]
env_prop [definition, in MetaRocq.Template.Typing]
env_error_sind [definition, in MetaRocq.Template.Checker]
env_error_rec [definition, in MetaRocq.Template.Checker]
env_error_ind [definition, in MetaRocq.Template.Checker]
env_error_rect [definition, in MetaRocq.Template.Checker]
env_error [inductive, in MetaRocq.Template.Checker]
env_closed_dearg [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
env_eq [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
EOptimizePropDiscr [library]
EPretty [library]
EPrimitive [library]
EPrimitiveFlags [record, in MetaRocq.Erasure.EWellformed]
eprogram [definition, in MetaRocq.Erasure.EProgram]
EProgram [library]
eprogram_env [definition, in MetaRocq.Erasure.EProgram]
eqb [definition, in MetaRocq.Utils.ByteCompare]
eqb [projection, in MetaRocq.Utils.ReflectEq]
eqbrs_refl [instance, in MetaRocq.PCUIC.PCUICConversion]
eqb_compare [definition, in MetaRocq.Utils.ByteCompareSpec]
eqb_global_decl [definition, in MetaRocq.Erasure.EReflect]
eqb_mutual_inductive_body [definition, in MetaRocq.Erasure.EReflect]
eqb_one_inductive_body [definition, in MetaRocq.Erasure.EReflect]
eqb_projection_body [definition, in MetaRocq.Erasure.EReflect]
eqb_constructor_body [definition, in MetaRocq.Erasure.EReflect]
eqb_constant_body [definition, in MetaRocq.Erasure.EReflect]
eqb_sort_ [definition, in MetaRocq.Common.Universes]
eqb_true_iff [lemma, in MetaRocq.Common.Universes]
eqb_ctx_spec [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_term_refl [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_term_spec [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_term [definition, in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_termp [definition, in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_termp_napp_spec [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_termp_napp [definition, in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_ctx [definition, in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_ctx_gen_proper [definition, in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_binder_annot_spec [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_ctx_upto [definition, in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_context_gen [abbreviation, in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_decl_gen [definition, in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_term_upto_univ_refl [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_term_upto_univ_proper [definition, in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_term_upto_univ_impl [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_univ_reflect [definition, in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_annots_reflect [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_annots_spec [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_annot_refl [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_annot_reflect [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_annot_spec [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_term_upto_univ [abbreviation, in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_term_upto_univ_napp [definition, in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_context_upto_names [abbreviation, in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_decl_upto_names [definition, in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_binder_annots [definition, in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_Variance [definition, in MetaRocq.Common.Reflect]
eqb_allowed_eliminations [definition, in MetaRocq.Common.Reflect]
eqb_sorts_decl [definition, in MetaRocq.Common.Reflect]
eqb_ConstraintType [definition, in MetaRocq.Common.Reflect]
eqb_recursivity_kind [definition, in MetaRocq.Common.Reflect]
eqb_context_decl [definition, in MetaRocq.Common.Reflect]
eqb_case_info [definition, in MetaRocq.Common.Reflect]
eqb_of_listable_spec [lemma, in MetaRocq.Utils.MRListable]
eqb_of_listable_eq [lemma, in MetaRocq.Utils.MRListable]
eqb_of_listable_bl [lemma, in MetaRocq.Utils.MRListable]
eqb_of_listable_lb [lemma, in MetaRocq.Utils.MRListable]
eqb_of_listable_refl [lemma, in MetaRocq.Utils.MRListable]
eqb_of_listable [definition, in MetaRocq.Utils.MRListable]
eqb_annot_reflect [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
eqb_binder_annot [definition, in MetaRocq.Common.BasicAst]
eqb_predicate [definition, in MetaRocq.PCUIC.PCUICAst]
eqb_predicate_gen [definition, in MetaRocq.PCUIC.PCUICAst]
eqb_term_conv [abbreviation, in MetaRocq.SafeChecker.PCUICSafeChecker]
eqb_global_decl [definition, in MetaRocq.Template.ReflectAst]
eqb_mutual_inductive_body [definition, in MetaRocq.Template.ReflectAst]
eqb_one_inductive_body [definition, in MetaRocq.Template.ReflectAst]
eqb_projection_body [definition, in MetaRocq.Template.ReflectAst]
eqb_constructor_body [definition, in MetaRocq.Template.ReflectAst]
eqb_constant_body [definition, in MetaRocq.Template.ReflectAst]
eqb_ctx [instance, in MetaRocq.Template.ReflectAst]
eqb_universe_instance_complete [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
eqb_universe_instance_spec [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
eqb_universe_instance [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
eqb_term_stack [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
eqb_term [abbreviation, in MetaRocq.SafeChecker.PCUICSafeConversion]
eqb_ctx [abbreviation, in MetaRocq.SafeChecker.PCUICSafeConversion]
eqb_univ_instance [definition, in MetaRocq.Common.uGraph]
eqb_univ_instance_gen [definition, in MetaRocq.Common.uGraph]
eqb_global_decl [definition, in MetaRocq.PCUIC.Syntax.PCUICReflect]
eqb_mutual_inductive_body [definition, in MetaRocq.PCUIC.Syntax.PCUICReflect]
eqb_one_inductive_body [definition, in MetaRocq.PCUIC.Syntax.PCUICReflect]
eqb_projection_body [definition, in MetaRocq.PCUIC.Syntax.PCUICReflect]
eqb_constructor_body [definition, in MetaRocq.PCUIC.Syntax.PCUICReflect]
eqb_constant_body [definition, in MetaRocq.PCUIC.Syntax.PCUICReflect]
eqb_context_decl [definition, in MetaRocq.PCUIC.Syntax.PCUICReflect]
eqb_predicate [definition, in MetaRocq.PCUIC.Syntax.PCUICReflect]
eqb_ctx [instance, in MetaRocq.PCUIC.Syntax.PCUICReflect]
eqb_term_reflect [instance, in MetaRocq.PCUIC.Syntax.PCUICReflect]
eqb_term [definition, in MetaRocq.PCUIC.Syntax.PCUICReflect]
eqb_predicate [definition, in MetaRocq.Template.Ast]
eqb_list [definition, in MetaRocq.Utils.ReflectEq]
eqb_refl [lemma, in MetaRocq.Utils.ReflectEq]
eqb_eq [lemma, in MetaRocq.Utils.ReflectEq]
eqb_specT [lemma, in MetaRocq.Utils.ReflectEq]
eqb_spec [projection, in MetaRocq.Utils.ReflectEq]
eqb_prim_val [definition, in MetaRocq.Erasure.EPrimitive]
eqb_prim_model [definition, in MetaRocq.Erasure.EPrimitive]
eqb_array [definition, in MetaRocq.Erasure.EPrimitive]
eqb_prim_val [definition, in MetaRocq.PCUIC.utils.PCUICPrimitive]
eqb_prim_model [definition, in MetaRocq.PCUIC.utils.PCUICPrimitive]
eqb_array [definition, in MetaRocq.PCUIC.utils.PCUICPrimitive]
EqDec_term [instance, in MetaRocq.Erasure.EReflect]
EqDec_stack_entry [instance, in MetaRocq.PCUIC.Syntax.PCUICPosition]
EqDec_branch_hole [instance, in MetaRocq.PCUIC.Syntax.PCUICPosition]
EqDec_predicate_hole [instance, in MetaRocq.PCUIC.Syntax.PCUICPosition]
EqDec_context_decl_hole [instance, in MetaRocq.PCUIC.Syntax.PCUICPosition]
EqDec_def_hole [instance, in MetaRocq.PCUIC.Syntax.PCUICPosition]
eqdec_binder_annot [instance, in MetaRocq.Common.BasicAst]
EqDec_term [instance, in MetaRocq.Template.ReflectAst]
EqDec_pstring [instance, in MetaRocq.Template.ReflectAst]
EqDec_term [instance, in MetaRocq.PCUIC.Syntax.PCUICReflect]
EqDec_ReflectEq [definition, in MetaRocq.Utils.ReflectEq]
eqt [abbreviation, in MetaRocq.PCUIC.PCUICSN]
eqt [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
eqt_refl [instance, in MetaRocq.SafeChecker.PCUICSafeConversion]
eqt_eqterm [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
EqualityDecGen [section, in MetaRocq.SafeChecker.PCUICEqualityDec]
EqualityDecGen.cf [variable, in MetaRocq.SafeChecker.PCUICEqualityDec]
EqualityDecGen.G [variable, in MetaRocq.SafeChecker.PCUICEqualityDec]
EqualityDecGen.HG [variable, in MetaRocq.SafeChecker.PCUICEqualityDec]
EqualityDecGen.hΣ [variable, in MetaRocq.SafeChecker.PCUICEqualityDec]
EqualityDecGen.uctx [variable, in MetaRocq.SafeChecker.PCUICEqualityDec]
EqualityDecGen.uctx' [variable, in MetaRocq.SafeChecker.PCUICEqualityDec]
EqualityDecGen.Σ [variable, in MetaRocq.SafeChecker.PCUICEqualityDec]
EqualityLemmas [section, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
EqualityLemmas.cf [variable, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
EqualityLemmas.wfΣ [variable, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
EqualityLemmas.Σ [variable, in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
equal_subst_instance_cstrs_mono [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
Equal_graph_edges [lemma, in MetaRocq.Common.uGraph]
equal_graph_equiv [instance, in MetaRocq.Common.uGraph]
Equal_graph [definition, in MetaRocq.Common.uGraph]
Equations [library]
Equations [library]
equiv_env_inter_hlookup [lemma, in MetaRocq.Erasure.ErasureFunction]
equiv_env_inter_sym [lemma, in MetaRocq.Erasure.ErasureFunction]
equiv_env_inter [definition, in MetaRocq.Erasure.ErasureFunction]
equiv_decls_inter [definition, in MetaRocq.Erasure.ErasureFunction]
equiv_reflect [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
equiv_reflectT [lemma, in MetaRocq.Utils.MRReflect]
equiv_True [instance, in MetaRocq.PCUIC.PCUICCumulProp]
equiv_eq_univ_prop [instance, in MetaRocq.PCUIC.PCUICCumulProp]
eq_term_eq_termp [lemma, in MetaRocq.PCUIC.PCUICCumulativity]
eq_termp [abbreviation, in MetaRocq.PCUIC.PCUICCumulativity]
eq_termp_napp [definition, in MetaRocq.PCUIC.PCUICCumulativity]
eq_term_mkApps [lemma, in MetaRocq.PCUIC.PCUICCumulativity]
eq_term_eq_term_napp [lemma, in MetaRocq.PCUIC.PCUICCumulativity]
eq_term_App [lemma, in MetaRocq.PCUIC.PCUICCumulativity]
eq_term_valid_pos [lemma, in MetaRocq.PCUIC.Syntax.PCUICPosition]
eq_term_upto_valid_pos [lemma, in MetaRocq.PCUIC.Syntax.PCUICPosition]
eq_context_upto_context_choice_term [lemma, in MetaRocq.PCUIC.Syntax.PCUICPosition]
eq_context_upto_names_upto_names [lemma, in MetaRocq.PCUIC.PCUICSR]
eq_ws_cumul_pb_terms_trans [lemma, in MetaRocq.PCUIC.PCUICSR]
eq_ws_cumul_pb_trans [lemma, in MetaRocq.PCUIC.PCUICSR]
eq_context_alpha_to_extended_list [lemma, in MetaRocq.PCUIC.PCUICSR]
eq_context_alpha_reln [lemma, in MetaRocq.PCUIC.PCUICSR]
eq_context_alpha_conv [lemma, in MetaRocq.PCUIC.PCUICSR]
eq_form [lemma, in MetaRocq.Examples.tauto]
eq_var [lemma, in MetaRocq.Examples.tauto]
eq_term_nl_eq [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
eq_context_nl [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
eq_context_nl_IH [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
eq_context_upto_names_eq_context_alpha [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
eq_context_upto_names_smash_context [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_context_upto_names_fold [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_context_upto_names_map2_set_binder_name_eq [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_context_upto_names_map2_set_binder_name [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_context_gen_map2_set_binder_name [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_annots_inst_case_context [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_annots_subst_instance_ctx [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_annots_lift_context [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_annots_subst_context [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_annots_fold [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_context_upto_names_binder_annot [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_annots [abbreviation, in MetaRocq.PCUIC.PCUICEquality]
eq_context_upto_flip [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_napp_flip [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_mkApps_inv [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_term_it_mkLambda_or_LetIn_inv [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_term_it_mkProd_or_LetIn [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_it_mkProd_or_LetIn [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_term_it_mkLambda_or_LetIn [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_it_mkLambda_or_LetIn_r [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_it_mkLambda_or_LetIn [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_context_impl [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_context_upto_nth_error [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_context_upto_smash_context [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_context_upto_subst_context [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_context_upto_length [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_context_upto_rev' [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_context_upto_rev [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_context_upto_cat [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_context_upto_sym [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_context_upto_refl [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_context_upto_impl [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_decl_upto_gen [definition, in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_isApp [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_mkApps_r_inv [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_mkApps_l_inv [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_mkApps [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_napp_mkApps_r_inv [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_napp_mkApps_l_inv [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_napp_mkApps [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_term_eq_term_napp [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_subst [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_substs [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_context_upto_lift_context [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_lift [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_term_leq_term [instance, in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_leq [instance, in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_empty_impl [instance, in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_impl [instance, in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_antisym [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_term_equiv [instance, in MetaRocq.PCUIC.PCUICEquality]
eq_context_equiv [instance, in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_equiv [instance, in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_trans [instance, in MetaRocq.PCUIC.PCUICEquality]
eq_predicate_trans [instance, in MetaRocq.PCUIC.PCUICEquality]
eq_predicate_sym [instance, in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_sym [instance, in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_refl [instance, in MetaRocq.PCUIC.PCUICEquality]
eq_mfixpoint_refl [instance, in MetaRocq.PCUIC.PCUICEquality]
eq_branches_refl [instance, in MetaRocq.PCUIC.PCUICEquality]
eq_predicate_refl [instance, in MetaRocq.PCUIC.PCUICEquality]
eq_binder_relevances_refl [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_binder_annot_refl [definition, in MetaRocq.PCUIC.PCUICEquality]
eq_binder_annot_equiv [instance, in MetaRocq.PCUIC.PCUICEquality]
eq_context_upto [abbreviation, in MetaRocq.PCUIC.PCUICEquality]
eq_context [abbreviation, in MetaRocq.PCUIC.PCUICEquality]
eq_decl [abbreviation, in MetaRocq.PCUIC.PCUICEquality]
eq_term [abbreviation, in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ [abbreviation, in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_napp_sind [definition, in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_napp_rec [definition, in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_napp_ind [definition, in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_napp_rect [definition, in MetaRocq.PCUIC.PCUICEquality]
eq_Prim [constructor, in MetaRocq.PCUIC.PCUICEquality]
eq_CoFix [constructor, in MetaRocq.PCUIC.PCUICEquality]
eq_Fix [constructor, in MetaRocq.PCUIC.PCUICEquality]
eq_Proj [constructor, in MetaRocq.PCUIC.PCUICEquality]
eq_Case [constructor, in MetaRocq.PCUIC.PCUICEquality]
eq_LetIn [constructor, in MetaRocq.PCUIC.PCUICEquality]
eq_Prod [constructor, in MetaRocq.PCUIC.PCUICEquality]
eq_Lambda [constructor, in MetaRocq.PCUIC.PCUICEquality]
eq_Construct [constructor, in MetaRocq.PCUIC.PCUICEquality]
eq_Ind [constructor, in MetaRocq.PCUIC.PCUICEquality]
eq_Const [constructor, in MetaRocq.PCUIC.PCUICEquality]
eq_App [constructor, in MetaRocq.PCUIC.PCUICEquality]
eq_Sort [constructor, in MetaRocq.PCUIC.PCUICEquality]
eq_Var [constructor, in MetaRocq.PCUIC.PCUICEquality]
eq_Evar [constructor, in MetaRocq.PCUIC.PCUICEquality]
eq_Rel [constructor, in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_napp [inductive, in MetaRocq.PCUIC.PCUICEquality]
eq_mfixpoint [definition, in MetaRocq.PCUIC.PCUICEquality]
eq_branches [definition, in MetaRocq.PCUIC.PCUICEquality]
eq_branch [definition, in MetaRocq.PCUIC.PCUICEquality]
eq_predicate [definition, in MetaRocq.PCUIC.PCUICEquality]
eq_context_trans [instance, in MetaRocq.PCUIC.PCUICEquality]
eq_context_sym [instance, in MetaRocq.PCUIC.PCUICEquality]
eq_context_refl [instance, in MetaRocq.PCUIC.PCUICEquality]
eq_decl_upto_names_trans [instance, in MetaRocq.PCUIC.PCUICEquality]
eq_decl_upto_names_sym [instance, in MetaRocq.PCUIC.PCUICEquality]
eq_decl_upto_names_refl [instance, in MetaRocq.PCUIC.PCUICEquality]
eq_context_gen_impl [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_context_upto_names_gen [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_decl_upto_names_gen [lemma, in MetaRocq.PCUIC.PCUICEquality]
eq_context_gen [abbreviation, in MetaRocq.PCUIC.PCUICEquality]
eq_context_upto_names [abbreviation, in MetaRocq.PCUIC.PCUICEquality]
eq_decl_upto_names_sind [definition, in MetaRocq.PCUIC.PCUICEquality]
eq_decl_upto_names_rec [definition, in MetaRocq.PCUIC.PCUICEquality]
eq_decl_upto_names_ind [definition, in MetaRocq.PCUIC.PCUICEquality]
eq_decl_upto_names_rect [definition, in MetaRocq.PCUIC.PCUICEquality]
eq_decl_upto_names [inductive, in MetaRocq.PCUIC.PCUICEquality]
eq_rect_transport [lemma, in MetaRocq.Utils.MREquality]
eq_univ_prop_compare_sort_propositional_r [lemma, in MetaRocq.PCUIC.PCUICElimination]
eq_univ_prop_compare_sort_propositional [lemma, in MetaRocq.PCUIC.PCUICElimination]
eq_sort_config_impl [lemma, in MetaRocq.Common.Universes]
eq_universe_config_impl [lemma, in MetaRocq.Common.Universes]
eq_sort_subset [lemma, in MetaRocq.Common.Universes]
eq_leq_sort' [definition, in MetaRocq.Common.Universes]
eq_sort_equivalence [instance, in MetaRocq.Common.Universes]
eq_leq_sort [instance, in MetaRocq.Common.Universes]
eq_sort_trans [instance, in MetaRocq.Common.Universes]
eq_sort_sym [instance, in MetaRocq.Common.Universes]
eq_sort_refl [instance, in MetaRocq.Common.Universes]
eq_sort [definition, in MetaRocq.Common.Universes]
eq_sort_ [definition, in MetaRocq.Common.Universes]
eq_universe_subset [lemma, in MetaRocq.Common.Universes]
eq_leq_universe' [definition, in MetaRocq.Common.Universes]
eq_universe_equivalence [instance, in MetaRocq.Common.Universes]
eq_leq_universe [instance, in MetaRocq.Common.Universes]
eq_universe_leq_universe [lemma, in MetaRocq.Common.Universes]
eq_universe_trans [instance, in MetaRocq.Common.Universes]
eq_universe_sym [instance, in MetaRocq.Common.Universes]
eq_universe_refl [instance, in MetaRocq.Common.Universes]
eq_universe [definition, in MetaRocq.Common.Universes]
eq_term_upto_univ_weaken_env [instance, in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
eq_term_subset [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
eq_term_upto_univ_mkApps [lemma, in MetaRocq.Template.TermEquality]
eq_term_App [lemma, in MetaRocq.Template.TermEquality]
eq_term_upto_univ_App [lemma, in MetaRocq.Template.TermEquality]
eq_term_leq_term [lemma, in MetaRocq.Template.TermEquality]
eq_term_upto_univ_morphism [lemma, in MetaRocq.Template.TermEquality]
eq_term_upto_univ_morphism0 [lemma, in MetaRocq.Template.TermEquality]
eq_term_upto_univ_impl [instance, in MetaRocq.Template.TermEquality]
eq_term_refl [lemma, in MetaRocq.Template.TermEquality]
eq_term_upto_univ_refl [lemma, in MetaRocq.Template.TermEquality]
eq_binder_annots_refl [instance, in MetaRocq.Template.TermEquality]
eq_binder_annot_refl [definition, in MetaRocq.Template.TermEquality]
eq_binder_annot_equiv [instance, in MetaRocq.Template.TermEquality]
eq_term [abbreviation, in MetaRocq.Template.TermEquality]
eq_term_upto_univ [abbreviation, in MetaRocq.Template.TermEquality]
eq_term_upto_univ_napp_sind [definition, in MetaRocq.Template.TermEquality]
eq_term_upto_univ_napp_rec [definition, in MetaRocq.Template.TermEquality]
eq_term_upto_univ_napp_ind [definition, in MetaRocq.Template.TermEquality]
eq_term_upto_univ_napp_rect [definition, in MetaRocq.Template.TermEquality]
eq_Array [constructor, in MetaRocq.Template.TermEquality]
eq_String [constructor, in MetaRocq.Template.TermEquality]
eq_Float [constructor, in MetaRocq.Template.TermEquality]
eq_Int [constructor, in MetaRocq.Template.TermEquality]
eq_Cast [constructor, in MetaRocq.Template.TermEquality]
eq_CoFix [constructor, in MetaRocq.Template.TermEquality]
eq_Fix [constructor, in MetaRocq.Template.TermEquality]
eq_Proj [constructor, in MetaRocq.Template.TermEquality]
eq_Case [constructor, in MetaRocq.Template.TermEquality]
eq_LetIn [constructor, in MetaRocq.Template.TermEquality]
eq_Prod [constructor, in MetaRocq.Template.TermEquality]
eq_Lambda [constructor, in MetaRocq.Template.TermEquality]
eq_Construct [constructor, in MetaRocq.Template.TermEquality]
eq_Ind [constructor, in MetaRocq.Template.TermEquality]
eq_Const [constructor, in MetaRocq.Template.TermEquality]
eq_App [constructor, in MetaRocq.Template.TermEquality]
eq_Sort [constructor, in MetaRocq.Template.TermEquality]
eq_Var [constructor, in MetaRocq.Template.TermEquality]
eq_Evar [constructor, in MetaRocq.Template.TermEquality]
eq_Rel [constructor, in MetaRocq.Template.TermEquality]
eq_term_upto_univ_napp [inductive, in MetaRocq.Template.TermEquality]
eq_context_upto_names [abbreviation, in MetaRocq.Template.TermEquality]
eq_decl_upto_names_sind [definition, in MetaRocq.Template.TermEquality]
eq_decl_upto_names_rec [definition, in MetaRocq.Template.TermEquality]
eq_decl_upto_names_ind [definition, in MetaRocq.Template.TermEquality]
eq_decl_upto_names_rect [definition, in MetaRocq.Template.TermEquality]
eq_decl_upto_names [inductive, in MetaRocq.Template.TermEquality]
eq_term [abbreviation, in MetaRocq.SafeChecker.PCUICEqualityDec]
eq_sortP_gen [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
eq_universeP_gen [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
eq_term_upto_univ_refl_wf [definition, in MetaRocq.SafeChecker.PCUICEqualityDec]
eq_dec_to_bool_refl [lemma, in MetaRocq.SafeChecker.PCUICEqualityDec]
eq_decl_reflect [instance, in MetaRocq.Common.Reflect]
eq_cast_kind [definition, in MetaRocq.Common.Reflect]
eq_def [definition, in MetaRocq.Common.Reflect]
eq_aname [definition, in MetaRocq.Common.Reflect]
eq_relevance [definition, in MetaRocq.Common.Reflect]
eq_name [definition, in MetaRocq.Common.Reflect]
eq_levels [definition, in MetaRocq.Common.Reflect]
eq_prop_level [definition, in MetaRocq.Common.Reflect]
eq_sort_dec [definition, in MetaRocq.Common.UniversesDec]
eq_sort__dec [definition, in MetaRocq.Common.UniversesDec]
eq_universe_dec [definition, in MetaRocq.Common.UniversesDec]
eq_context_cumul_Spec_rel [lemma, in MetaRocq.PCUIC.Typing.PCUICContextConversionTyp]
eq_context_cumul_Spec [lemma, in MetaRocq.PCUIC.Typing.PCUICContextConversionTyp]
eq_term_set_binder_name [lemma, in MetaRocq.PCUIC.PCUICValidity]
eq_binder_annots_eq_ctx [lemma, in MetaRocq.PCUIC.PCUICValidity]
eq_context_upto_univ_cumul_context [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
eq_context_upto_univ_conv_context [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
eq_context_upto_names_conv_context [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
eq_subrel_eq_sort [instance, in MetaRocq.PCUIC.PCUICContextConversion]
eq_subrel_eq_univ [instance, in MetaRocq.PCUIC.PCUICContextConversion]
eq_context_upto_cumul_context [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
eq_context_upto_conv_context [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
eq_context_upto_cumul_pb_context [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
eq_leq_context_upto [lemma, in MetaRocq.PCUIC.PCUICContextConversion]
eq_term_upto_univ_napp_on_free_vars [lemma, in MetaRocq.PCUIC.PCUICConfluence]
eq_context_upto_names_red_ctx_alpha [lemma, in MetaRocq.PCUIC.PCUICConfluence]
eq_context_upto_names_red_ctx [lemma, in MetaRocq.PCUIC.PCUICConfluence]
eq_context_upto_names_app [lemma, in MetaRocq.PCUIC.PCUICConfluence]
eq_context_upto_names_on_free_vars [lemma, in MetaRocq.PCUIC.PCUICConfluence]
eq_context_upto_names_subst_instance [lemma, in MetaRocq.PCUIC.PCUICConfluence]
eq_context_upto_univ_subst_instance' [lemma, in MetaRocq.PCUIC.PCUICConfluence]
eq_context_upto_univ_subst_instance [lemma, in MetaRocq.PCUIC.PCUICConfluence]
eq_term_upto_univ_subst_instance' [lemma, in MetaRocq.PCUIC.PCUICConfluence]
eq_context_upto_names_univ_subst_preserved [lemma, in MetaRocq.PCUIC.PCUICConfluence]
eq_context_upto_univ_subst_preserved [instance, in MetaRocq.PCUIC.PCUICConfluence]
eq_context_upto_names_eq_context_upto [lemma, in MetaRocq.PCUIC.PCUICConfluence]
eq_context_extended_subst [lemma, in MetaRocq.PCUIC.PCUICConfluence]
eq_context_gen_context_assumptions [lemma, in MetaRocq.PCUIC.PCUICConfluence]
eq_context_upto_names_extended_subst [lemma, in MetaRocq.PCUIC.PCUICConfluence]
eq_context_upto_names_context_assumptions [lemma, in MetaRocq.PCUIC.PCUICConfluence]
eq_one_decl [abbreviation, in MetaRocq.PCUIC.PCUICConfluence]
eq_annots_expand_lets_ctx [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
eq_names_subst_instance_pcuic [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
eq_names_subst_context_pcuic [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
eq_term_upto_univ_expand_lets [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
eq_binder_trans [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
eq_names_smash_context [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
eq_term_inds [lemma, in MetaRocq.PCUIC.PCUICConversion]
eq_term_compare_term [lemma, in MetaRocq.PCUIC.PCUICConversion]
eq_context_upto_ws_cumul_ctx_pb [lemma, in MetaRocq.PCUIC.PCUICConversion]
eq_term_fix_or_cofix [lemma, in MetaRocq.PCUIC.PCUICConversion]
eq_context_upto_names_inst_case_context [lemma, in MetaRocq.PCUIC.PCUICConversion]
eq_context_upto_names_subst_context [lemma, in MetaRocq.PCUIC.PCUICConversion]
eq_term_upto_univ_conv_arity_r [lemma, in MetaRocq.PCUIC.PCUICConversion]
eq_term_upto_univ_conv_arity_l [lemma, in MetaRocq.PCUIC.PCUICConversion]
eq_terms_ws_cumul_pb_terms [lemma, in MetaRocq.PCUIC.PCUICConversion]
eq_term_upto_univ_cumulSpec [lemma, in MetaRocq.PCUIC.PCUICConversion]
eq_term_upto_univ_napp_cumulSpec [lemma, in MetaRocq.PCUIC.PCUICConversion]
eq_term_upto_univ_napp_0 [lemma, in MetaRocq.PCUIC.PCUICAlpha]
eq_context_conversion [lemma, in MetaRocq.PCUIC.PCUICAlpha]
eq_context_upto_names_eq_context_alpha [lemma, in MetaRocq.PCUIC.PCUICAlpha]
eq_context_upto_subst_instance [lemma, in MetaRocq.PCUIC.PCUICAlpha]
eq_context_upto_conv_context_rel [lemma, in MetaRocq.PCUIC.PCUICAlpha]
eq_context_upto_empty_impl [lemma, in MetaRocq.PCUIC.PCUICAlpha]
eq_term_upto_univ_rename [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
eq_eta_global_env [lemma, in MetaRocq.Erasure.Typed.CertifyingEta]
eq_pair_transport [lemma, in MetaRocq.PCUIC.Syntax.PCUICViews]
eq_names_subst_instance [lemma, in MetaRocq.PCUIC.PCUICContexts]
eq_names_subst_context [lemma, in MetaRocq.PCUIC.PCUICContexts]
eq_names [abbreviation, in MetaRocq.PCUIC.PCUICContexts]
eq_binder_annot [definition, in MetaRocq.Common.BasicAst]
eq_binder_annots_eq [lemma, in MetaRocq.PCUIC.PCUICCasesContexts]
eq_names_subst_instance [lemma, in MetaRocq.PCUIC.PCUICCasesContexts]
eq_names_subst_context [lemma, in MetaRocq.PCUIC.PCUICCasesContexts]
eq_names [abbreviation, in MetaRocq.PCUIC.PCUICCasesContexts]
eq_predicate [instance, in MetaRocq.Template.ReflectAst]
eq_context [definition, in MetaRocq.Template.Typing]
eq_decl [definition, in MetaRocq.Template.Typing]
eq_opt_term [definition, in MetaRocq.Template.Typing]
eq_term_nocast [definition, in MetaRocq.Template.Typing]
eq_term [definition, in MetaRocq.Template.Checker]
eq_case_info [definition, in MetaRocq.Template.Checker]
eq_max [definition, in MetaRocq.Utils.wGraph]
eq_projection_refl [lemma, in MetaRocq.Common.Kernames]
eq_projection [definition, in MetaRocq.Common.Kernames]
eq_inductive_refl [lemma, in MetaRocq.Common.Kernames]
eq_inductive [abbreviation, in MetaRocq.Common.Kernames]
eq_inductive_def [definition, in MetaRocq.Common.Kernames]
eq_constant [definition, in MetaRocq.Common.Kernames]
eq_kername_refl [lemma, in MetaRocq.Common.Kernames]
eq_kername [abbreviation, in MetaRocq.Common.Kernames]
eq_term_napp [abbreviation, in MetaRocq.PCUIC.PCUICCumulProp]
eq_term_prop_mkApps_inv [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
eq_term_eq_term_prop_impl [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
eq_term_prop_impl [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
eq_term_prop [definition, in MetaRocq.PCUIC.PCUICCumulProp]
eq_univ_prop [definition, in MetaRocq.PCUIC.PCUICCumulProp]
eq_tip_skipn [lemma, in MetaRocq.Template.TypingWf]
eq_decompose_app [lemma, in MetaRocq.Template.TypingWf]
eq_context_upto_subst_preserved [instance, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
eq_term_subst_instance [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
eq_term_upto_univ_subst_preserved [instance, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
eq_sort_subst_instance [instance, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
eq_universe_subst_instance [instance, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
eq_universe_SubstUnivPreserving [instance, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
eq_term_upto_univ_subst_instance [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
eq_valuation [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
eq_termp_mkApps_inv [lemma, in MetaRocq.PCUIC.PCUICConvCumInversion]
eq_term_upto_univ_napp_nonind [lemma, in MetaRocq.PCUIC.PCUICConvCumInversion]
eq_term_eq_termp [lemma, in MetaRocq.PCUIC.PCUICConvCumInversion]
eq_kername_eq [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
eq_term_config_impl [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningConfigConv]
eq_term [abbreviation, in MetaRocq.SafeChecker.PCUICSafeConversion]
eq_term_valid_pos [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
eq_context_upto_inst_case_context [lemma, in MetaRocq.PCUIC.PCUICPrincipality]
eq_context_empty_eq_context [lemma, in MetaRocq.PCUIC.PCUICPrincipality]
eq_term_empty_eq_term [lemma, in MetaRocq.PCUIC.PCUICPrincipality]
eq_term_empty_leq_term [lemma, in MetaRocq.PCUIC.PCUICPrincipality]
eq_term_leq_term [lemma, in MetaRocq.PCUIC.PCUICPrincipality]
eq_context_gen_wf_branch [lemma, in MetaRocq.SafeChecker.PCUICTypeChecker]
eq_context_gen_wf_predicate [lemma, in MetaRocq.SafeChecker.PCUICTypeChecker]
eq_names_subst_instance_pcuic [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
eq_names_subst_context_pcuic [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
eq_binder_trans [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
eq_names_subst_instance [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
eq_names_subst_context [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
eq_names [abbreviation, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
eq_term_upto_univ_inst [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
eq_simpl_pred [definition, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
eq_annots_cstr_branch_context [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
eq_annots_ind_predicate_context [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
eq_annots_expand_lets_ctx [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
eq_binder_annot_eq_context_gen_set_binder_name [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
eq_ctx [instance, in MetaRocq.PCUIC.Syntax.PCUICReflect]
eq_prod_refl [lemma, in MetaRocq.Utils.ReflectEq]
eq_prod [definition, in MetaRocq.Utils.ReflectEq]
eq_sig_true [definition, in MetaRocq.Utils.ReflectEq]
eq_bool [definition, in MetaRocq.Utils.ReflectEq]
eq_list.eqA [variable, in MetaRocq.Utils.ReflectEq]
eq_list.A [variable, in MetaRocq.Utils.ReflectEq]
eq_list [section, in MetaRocq.Utils.ReflectEq]
eq_option [definition, in MetaRocq.Utils.ReflectEq]
eq_dec_to_bool [definition, in MetaRocq.Utils.ReflectEq]
eq0_leq0_universe [lemma, in MetaRocq.Common.Universes]
eq0_universe [definition, in MetaRocq.Common.Universes]
eq0_universe_dec [definition, in MetaRocq.Common.UniversesDec]
erasable_tBox_value [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
erase [definition, in MetaRocq.Erasure.ErasureFunction]
Erase [section, in MetaRocq.Erasure.ErasureFunction]
EraseEnv [section, in MetaRocq.Erasure.Typed.Erasure]
EraseEnv.fake_normalization [variable, in MetaRocq.Erasure.Typed.Erasure]
EraseEnv.fake_guard_correct [variable, in MetaRocq.Erasure.Typed.Erasure]
EraseGlobalFast [section, in MetaRocq.Erasure.ErasureFunctionProperties]
erases [inductive, in MetaRocq.Erasure.Extract]
erases_global_wf_glob [lemma, in MetaRocq.Erasure.ErasureCorrectness]
erases_mutual_inductive_body_wf [lemma, in MetaRocq.Erasure.ErasureCorrectness]
erases_global_decls_fresh [lemma, in MetaRocq.Erasure.ErasureCorrectness]
erases_global_closed_env [lemma, in MetaRocq.Erasure.ErasureCorrectness]
erases_correct [lemma, in MetaRocq.Erasure.ErasureCorrectness]
erases_lazy [lemma, in MetaRocq.Erasure.ErasureCorrectness]
erases_mutual [lemma, in MetaRocq.Erasure.ErasureFunction]
erases_weakening_env [lemma, in MetaRocq.Erasure.ErasureFunction]
erases_erase [lemma, in MetaRocq.Erasure.ErasureFunction]
erases_wellformed [lemma, in MetaRocq.Erasure.ErasureProperties]
erases_closed [lemma, in MetaRocq.Erasure.ErasureProperties]
erases_subst_instance_decl [lemma, in MetaRocq.Erasure.ErasureProperties]
erases_subst_instance'' [lemma, in MetaRocq.Erasure.ErasureProperties]
erases_subst_instance [lemma, in MetaRocq.Erasure.ErasureProperties]
erases_subst_instance0 [lemma, in MetaRocq.Erasure.ErasureProperties]
erases_context_conversion [lemma, in MetaRocq.Erasure.ErasureProperties]
erases_isLambda [lemma, in MetaRocq.Erasure.ErasureProperties]
erases_mkApps_inv [lemma, in MetaRocq.Erasure.ErasureProperties]
erases_mkApps [lemma, in MetaRocq.Erasure.ErasureProperties]
erases_App [lemma, in MetaRocq.Erasure.ErasureProperties]
erases_ext_eq [lemma, in MetaRocq.Erasure.ErasureProperties]
erases_firstorder' [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
erases_firstorder [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
erases_global_erase_global [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
erases_wf_fixpoints [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
erases_deps_wellformed [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
erases_deps_erase_weaken [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
erases_deps_erase [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
erases_deps_weaken [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
erases_global_erases_deps [lemma, in MetaRocq.Erasure.EDeps]
erases_global_all_deps [lemma, in MetaRocq.Erasure.EDeps]
erases_deps_single [lemma, in MetaRocq.Erasure.EDeps]
erases_declared_constructor [lemma, in MetaRocq.Erasure.EDeps]
erases_deps_cons [lemma, in MetaRocq.Erasure.EDeps]
erases_deps_forall_ind [lemma, in MetaRocq.Erasure.EDeps]
erases_deps_eval [lemma, in MetaRocq.Erasure.EDeps]
erases_deps_cunfold_cofix [lemma, in MetaRocq.Erasure.EDeps]
erases_deps_cunfold_fix [lemma, in MetaRocq.Erasure.EDeps]
erases_deps_substl [lemma, in MetaRocq.Erasure.EDeps]
erases_deps_csubst [lemma, in MetaRocq.Erasure.EDeps]
erases_deps_subst1 [lemma, in MetaRocq.Erasure.EDeps]
erases_deps_subst [lemma, in MetaRocq.Erasure.EDeps]
erases_deps_lift [lemma, in MetaRocq.Erasure.EDeps]
erases_deps_mkApps_inv [lemma, in MetaRocq.Erasure.EDeps]
erases_deps_mkApps [lemma, in MetaRocq.Erasure.EDeps]
erases_subst0 [lemma, in MetaRocq.Erasure.ESubstitution]
erases_subst [lemma, in MetaRocq.Erasure.ESubstitution]
erases_eq [lemma, in MetaRocq.Erasure.ESubstitution]
erases_weakening [lemma, in MetaRocq.Erasure.ESubstitution]
erases_weakening' [lemma, in MetaRocq.Erasure.ESubstitution]
erases_ctx_ext [lemma, in MetaRocq.Erasure.ESubstitution]
erases_extends' [lemma, in MetaRocq.Erasure.ESubstitution]
erases_extends [lemma, in MetaRocq.Erasure.ESubstitution]
erases_wf_inductives_mapping [lemma, in MetaRocq.ErasurePlugin.Erasure]
erases_global_lookup_env_none [lemma, in MetaRocq.ErasurePlugin.Erasure]
erases_global_lookup_env_inductive [lemma, in MetaRocq.ErasurePlugin.Erasure]
erases_global_lookup_env_constant [lemma, in MetaRocq.ErasurePlugin.Erasure]
erases_deps_sind [definition, in MetaRocq.Erasure.Extract]
erases_deps_ind [definition, in MetaRocq.Erasure.Extract]
erases_deps_tPrimArray [constructor, in MetaRocq.Erasure.Extract]
erases_deps_tPrimString [constructor, in MetaRocq.Erasure.Extract]
erases_deps_tPrimFloat [constructor, in MetaRocq.Erasure.Extract]
erases_deps_tPrimInt [constructor, in MetaRocq.Erasure.Extract]
erases_deps_tCoFix [constructor, in MetaRocq.Erasure.Extract]
erases_deps_tFix [constructor, in MetaRocq.Erasure.Extract]
erases_deps_tProj [constructor, in MetaRocq.Erasure.Extract]
erases_deps_tCase [constructor, in MetaRocq.Erasure.Extract]
erases_deps_tConstruct [constructor, in MetaRocq.Erasure.Extract]
erases_deps_tConst [constructor, in MetaRocq.Erasure.Extract]
erases_deps_tApp [constructor, in MetaRocq.Erasure.Extract]
erases_deps_tLetIn [constructor, in MetaRocq.Erasure.Extract]
erases_deps_tLambda [constructor, in MetaRocq.Erasure.Extract]
erases_deps_tEvar [constructor, in MetaRocq.Erasure.Extract]
erases_deps_tVar [constructor, in MetaRocq.Erasure.Extract]
erases_deps_tRel [constructor, in MetaRocq.Erasure.Extract]
erases_deps_tBox [constructor, in MetaRocq.Erasure.Extract]
erases_deps [inductive, in MetaRocq.Erasure.Extract]
erases_global [definition, in MetaRocq.Erasure.Extract]
erases_global_decls_sind [definition, in MetaRocq.Erasure.Extract]
erases_global_decls_ind [definition, in MetaRocq.Erasure.Extract]
erases_global_ind [constructor, in MetaRocq.Erasure.Extract]
erases_global_cnst [constructor, in MetaRocq.Erasure.Extract]
erases_global_nil [constructor, in MetaRocq.Erasure.Extract]
erases_global_decls [inductive, in MetaRocq.Erasure.Extract]
erases_mutual_inductive_body [definition, in MetaRocq.Erasure.Extract]
erases_one_inductive_body [definition, in MetaRocq.Erasure.Extract]
erases_constant_body [definition, in MetaRocq.Erasure.Extract]
erases_forall_list_ind [lemma, in MetaRocq.Erasure.Extract]
erases_sind [definition, in MetaRocq.Erasure.Extract]
erases_ind [definition, in MetaRocq.Erasure.Extract]
erases_box [constructor, in MetaRocq.Erasure.Extract]
erases_tPrim [constructor, in MetaRocq.Erasure.Extract]
erases_tCoFix [constructor, in MetaRocq.Erasure.Extract]
erases_tFix [constructor, in MetaRocq.Erasure.Extract]
erases_tProj [constructor, in MetaRocq.Erasure.Extract]
erases_tCase [constructor, in MetaRocq.Erasure.Extract]
erases_tConstruct [constructor, in MetaRocq.Erasure.Extract]
erases_tConst [constructor, in MetaRocq.Erasure.Extract]
erases_tApp [constructor, in MetaRocq.Erasure.Extract]
erases_tLetIn [constructor, in MetaRocq.Erasure.Extract]
erases_tLambda [constructor, in MetaRocq.Erasure.Extract]
erases_tEvar [constructor, in MetaRocq.Erasure.Extract]
erases_tVar [constructor, in MetaRocq.Erasure.Extract]
erases_tRel [constructor, in MetaRocq.Erasure.Extract]
erase_global_decls_recursive [definition, in MetaRocq.Erasure.Typed.Erasure]
erase_global_decls_deps_recursive [definition, in MetaRocq.Erasure.Typed.Erasure]
erase_global_decl [definition, in MetaRocq.Erasure.Typed.Erasure]
erase_ind [definition, in MetaRocq.Erasure.Typed.Erasure]
erase_ind_body [definition, in MetaRocq.Erasure.Typed.Erasure]
erase_ind_ctor [definition, in MetaRocq.Erasure.Typed.Erasure]
erase_ind_arity [definition, in MetaRocq.Erasure.Typed.Erasure]
erase_constant_decl [definition, in MetaRocq.Erasure.Typed.Erasure]
erase_arity [definition, in MetaRocq.Erasure.Typed.Erasure]
erase_type_scheme [definition, in MetaRocq.Erasure.Typed.Erasure]
erase_type_scheme_eta [definition, in MetaRocq.Erasure.Typed.Erasure]
erase_type_scheme_viewc [definition, in MetaRocq.Erasure.Typed.Erasure]
erase_type_scheme_view_sind [definition, in MetaRocq.Erasure.Typed.Erasure]
erase_type_scheme_view_rec [definition, in MetaRocq.Erasure.Typed.Erasure]
erase_type_scheme_view_ind [definition, in MetaRocq.Erasure.Typed.Erasure]
erase_type_scheme_view_rect [definition, in MetaRocq.Erasure.Typed.Erasure]
erase_type_scheme_view_other [constructor, in MetaRocq.Erasure.Typed.Erasure]
erase_type_scheme_view_lam [constructor, in MetaRocq.Erasure.Typed.Erasure]
erase_type_scheme_view [inductive, in MetaRocq.Erasure.Typed.Erasure]
erase_type [definition, in MetaRocq.Erasure.Typed.Erasure]
erase_type_aux [definition, in MetaRocq.Erasure.Typed.Erasure]
erase_type_viewc [definition, in MetaRocq.Erasure.Typed.Erasure]
erase_type_view_sind [definition, in MetaRocq.Erasure.Typed.Erasure]
erase_type_view_rec [definition, in MetaRocq.Erasure.Typed.Erasure]
erase_type_view_ind [definition, in MetaRocq.Erasure.Typed.Erasure]
erase_type_view_rect [definition, in MetaRocq.Erasure.Typed.Erasure]
erase_type_view [inductive, in MetaRocq.Erasure.Typed.Erasure]
erase_type_discr [definition, in MetaRocq.Erasure.Typed.Erasure]
erase_rel [definition, in MetaRocq.Erasure.Typed.Erasure]
erase_constant_body_correct' [lemma, in MetaRocq.Erasure.ErasureFunction]
erase_constant_body_correct [lemma, in MetaRocq.Erasure.ErasureFunction]
erase_global_irr [lemma, in MetaRocq.Erasure.ErasureFunction]
erase_global_deps_irr [lemma, in MetaRocq.Erasure.ErasureFunction]
erase_global [definition, in MetaRocq.Erasure.ErasureFunction]
erase_global_deps [definition, in MetaRocq.Erasure.ErasureFunction]
erase_constant_decl_irrel [lemma, in MetaRocq.Erasure.ErasureFunction]
erase_constant_decl [definition, in MetaRocq.Erasure.ErasureFunction]
erase_constant_body_irrel [lemma, in MetaRocq.Erasure.ErasureFunction]
erase_irrel_global_env [lemma, in MetaRocq.Erasure.ErasureFunction]
erase_mutual_inductive_body [definition, in MetaRocq.Erasure.ErasureFunction]
erase_one_inductive_body [definition, in MetaRocq.Erasure.ErasureFunction]
erase_constant_body [definition, in MetaRocq.Erasure.ErasureFunction]
erase_to_box [lemma, in MetaRocq.Erasure.ErasureFunction]
erase_terms_eq [lemma, in MetaRocq.Erasure.ErasureFunction]
erase_irrel [lemma, in MetaRocq.Erasure.ErasureFunction]
erase_cofix [definition, in MetaRocq.Erasure.ErasureFunction]
erase_fix [definition, in MetaRocq.Erasure.ErasureFunction]
erase_brs [definition, in MetaRocq.Erasure.ErasureFunction]
erase_terms [definition, in MetaRocq.Erasure.ErasureFunction]
erase_constant_decl_impl [definition, in MetaRocq.Erasure.Typed.TypeAnnotations]
erase_type_of [definition, in MetaRocq.Erasure.Typed.TypeAnnotations]
erase_type_aux_impl [definition, in MetaRocq.Erasure.Typed.TypeAnnotations]
erase_global_decls_deps_recursive_correct [lemma, in MetaRocq.Erasure.Typed.ErasureCorrectness]
erase_global_decls_deps_recursive_correct_gen [lemma, in MetaRocq.Erasure.Typed.ErasureCorrectness]
erase_ind_correct [lemma, in MetaRocq.Erasure.Typed.ErasureCorrectness]
erase_ind_body_wellformed [lemma, in MetaRocq.Erasure.Typed.ErasureCorrectness]
erase_ind_body_correct [lemma, in MetaRocq.Erasure.Typed.ErasureCorrectness]
erase_wellformed_fast [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
erase_global_fast_wf_glob [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
erase_global_fast [definition, in MetaRocq.Erasure.ErasureFunctionProperties]
erase_global_deps_fast_erase_global_deps [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
erase_global_deps_fast_spec [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
erase_global_deps_fast_spec_gen [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
erase_global_deps_fast [definition, in MetaRocq.Erasure.ErasureFunctionProperties]
erase_correct_firstorder [definition, in MetaRocq.Erasure.ErasureFunctionProperties]
erase_correct_strong [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
erase_correct_strong' [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
erase_eval_to_box_eager [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
erase_eval_to_box [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
erase_global_deps_eval [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
erase_global_wf_glob [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
erase_global_ind_decl_wf_glob' [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
erase_global_cst_wf_glob [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
erase_constant_body_correct_glob [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
erase_global_deps_wf_glob [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
erase_global_ind_decl_wf_glob [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
erase_global_cst_decl_wf_glob [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
erase_constant_body_correct'' [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
erase_wellformed_weaken [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
erase_wellformed_deps [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
erase_global_wellformed [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
erase_wf_fixpoints [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
erase_global_closed [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
erase_cofix_eq [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
erase_fix_eq [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
erase_brs_eq [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
erase_global_fresh [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
erase_global_deps_fresh [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
erase_global_declared_constructor [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
erase_global_deps_erase_global [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
erase_constant_decl_deps [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
erase_mkApps [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
erase_correct [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
erase_global_includes [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
erase_global_erases_deps [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
erase_eta_app [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
erase_nin [definition, in MetaRocq.ErasurePlugin.ErasureCorrectness]
erase_function_to_function [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
erase_function [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
erase_transform_fo [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
erase_transform_fo_gen [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
erase_tranform_firstorder [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
erase_decl_equal [definition, in MetaRocq.ErasurePlugin.ErasureCorrectness]
erase_preserves_inductives [definition, in MetaRocq.ErasurePlugin.ErasureCorrectness]
erase_term [definition, in MetaRocq.Erasure.Typed.ExtractionCorrectness]
erase_env [definition, in MetaRocq.Erasure.Typed.ExtractionCorrectness]
erase_erasable [lemma, in MetaRocq.Erasure.Typed.ExtractionCorrectness]
erase_program_typed [definition, in MetaRocq.ErasurePlugin.ETransform]
erase_transform [definition, in MetaRocq.ErasurePlugin.ETransform]
erase_program [definition, in MetaRocq.ErasurePlugin.ETransform]
erase_pcuic_program [definition, in MetaRocq.ErasurePlugin.ETransform]
erase_pcuic_program_normalization_helper [lemma, in MetaRocq.ErasurePlugin.ETransform]
erase_and_print_template_program [definition, in MetaRocq.ErasurePlugin.Erasure]
erase_transform_mapping [definition, in MetaRocq.ErasurePlugin.Erasure]
erase_prim_val_sind [definition, in MetaRocq.Erasure.Extract]
erase_prim_val_ind [definition, in MetaRocq.Erasure.Extract]
erase_prim [constructor, in MetaRocq.Erasure.Extract]
erase_prim_val [inductive, in MetaRocq.Erasure.Extract]
erase_prim_model_sind [definition, in MetaRocq.Erasure.Extract]
erase_prim_model_rec [definition, in MetaRocq.Erasure.Extract]
erase_prim_model_ind [definition, in MetaRocq.Erasure.Extract]
erase_prim_model_rect [definition, in MetaRocq.Erasure.Extract]
erase_primArray [constructor, in MetaRocq.Erasure.Extract]
erase_primString [constructor, in MetaRocq.Erasure.Extract]
erase_primFloat [constructor, in MetaRocq.Erasure.Extract]
erase_primInt [constructor, in MetaRocq.Erasure.Extract]
erase_prim_model [inductive, in MetaRocq.Erasure.Extract]
erase_context [definition, in MetaRocq.Erasure.Extract]
Erase.normalization_in [variable, in MetaRocq.Erasure.ErasureFunction]
Erase.X [variable, in MetaRocq.Erasure.ErasureFunction]
Erase.X_type [variable, in MetaRocq.Erasure.ErasureFunction]
Erasure [library]
Erasure [library]
ErasureCorrectness [library]
ErasureCorrectness [library]
ErasureCorrectness [library]
ErasureFunction [section, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ErasureFunction [library]
ErasureFunctionProperties [library]
ErasureProperties [library]
erasure_pipeline_extends_app [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
erasure_pipeline_mapping [definition, in MetaRocq.ErasurePlugin.Erasure]
erasure_pipeline [definition, in MetaRocq.ErasurePlugin.Erasure]
erasure_configuration [record, in MetaRocq.ErasurePlugin.Erasure]
EReflect [library]
ERemoveParams [library]
EReorderCstrs [library]
Err [constructor, in MetaRocq.Erasure.Typed.ResultMonad]
Error [constructor, in MetaRocq.SafeChecker.PCUICSafeConversion]
ESpineView [library]
ESubstitution [library]
Eta [section, in MetaRocq.Template.EtaExpand]
Eta [section, in MetaRocq.Erasure.Typed.CertifyingEta]
EtaExpand [library]
etaExp_csubst [lemma, in MetaRocq.Erasure.EEtaExpanded]
etaExp_fixsubst [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
etaExp_csubst [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
etaExp_csubst' [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
eta_byte [definition, in MetaRocq.Utils.ByteCompareSpec]
eta_expand_erase [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
eta_expand_global_env_expanded [lemma, in MetaRocq.Template.EtaExpand]
eta_context_assumptions [lemma, in MetaRocq.Template.EtaExpand]
eta_expand_global_decl_expanded [lemma, in MetaRocq.Template.EtaExpand]
eta_context_length [lemma, in MetaRocq.Template.EtaExpand]
eta_expand_context_sorts [lemma, in MetaRocq.Template.EtaExpand]
eta_expand_context [lemma, in MetaRocq.Template.EtaExpand]
eta_declared_constructor [lemma, in MetaRocq.Template.EtaExpand]
eta_lookup_global_error [lemma, in MetaRocq.Template.EtaExpand]
eta_lookup_global [lemma, in MetaRocq.Template.EtaExpand]
eta_expand_expanded [lemma, in MetaRocq.Template.EtaExpand]
eta_expand_program [definition, in MetaRocq.Template.EtaExpand]
eta_expand_global_env [definition, in MetaRocq.Template.EtaExpand]
eta_global_declarations [definition, in MetaRocq.Template.EtaExpand]
eta_global_declaration [definition, in MetaRocq.Template.EtaExpand]
eta_minductive_decl [definition, in MetaRocq.Template.EtaExpand]
eta_inductive_decl [definition, in MetaRocq.Template.EtaExpand]
eta_constructor_decl [definition, in MetaRocq.Template.EtaExpand]
eta_context [definition, in MetaRocq.Template.EtaExpand]
eta_global_decl [definition, in MetaRocq.Template.EtaExpand]
eta_expand [definition, in MetaRocq.Template.EtaExpand]
eta_fixpoint [definition, in MetaRocq.Template.EtaExpand]
eta_constructor [definition, in MetaRocq.Template.EtaExpand]
eta_single [definition, in MetaRocq.Template.EtaExpand]
eta_expand_def [definition, in MetaRocq.Erasure.Typed.CertifyingEta]
eta_global_env_template [definition, in MetaRocq.Erasure.Typed.CertifyingEta]
eta_global_env [definition, in MetaRocq.Erasure.Typed.CertifyingEta]
eta_expand [definition, in MetaRocq.Erasure.Typed.CertifyingEta]
eta_const [definition, in MetaRocq.Erasure.Typed.CertifyingEta]
eta_ctor [definition, in MetaRocq.Erasure.Typed.CertifyingEta]
eta_single [definition, in MetaRocq.Erasure.Typed.CertifyingEta]
eta_expand [definition, in MetaRocq.Template.TemplateCheckWf]
eta_expand_mapping [definition, in MetaRocq.ErasurePlugin.Erasure]
eta_lookup_inductive_ctors [lemma, in MetaRocq.ErasurePlugin.Erasure]
eta_expand [definition, in MetaRocq.ErasurePlugin.Erasure]
eta_pair [lemma, in MetaRocq.SafeChecker.PCUICSafeConversion]
Eta.constants [variable, in MetaRocq.Erasure.Typed.CertifyingEta]
Eta.ctors [variable, in MetaRocq.Erasure.Typed.CertifyingEta]
Eta.Σ [variable, in MetaRocq.Template.EtaExpand]
Eta.Σ [variable, in MetaRocq.Erasure.Typed.CertifyingEta]
ETermFlags [record, in MetaRocq.Erasure.EWellformed]
ETransform [library]
ETransformPresAppLam [module, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.Comp [section, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.compose [instance, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.Comp.env [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.Comp.env' [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.Comp.env'' [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.Comp.eval [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.Comp.eval' [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.Comp.eval'' [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.Comp.hpp [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.Comp.is_etaexp'' [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.Comp.is_etaexp' [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.Comp.is_etaexp [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.Comp.o [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.Comp.oext [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.Comp.o' [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.Comp.o'ext [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.Opt [section, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.Opt.env [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.Opt.env' [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.Opt.eval [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.Opt.eval' [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.Opt.is_etaexp' [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.Opt.is_etaexp [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.Opt.o [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.t [record, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.transform_lam [projection, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.transform_app [projection, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.transform_etaexp [projection, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.transform_env_irrel [projection, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresAppLam.transform_pre_irrel [projection, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO [module, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Comp [section, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.compose [instance, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.compose_compile_fo_value [definition, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Comp.compile_fo_value' [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Comp.compile_fo_value [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Comp.env [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Comp.env' [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Comp.env'' [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Comp.eval [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Comp.eval' [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Comp.eval'' [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Comp.firstorder_value'' [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Comp.firstorder_value' [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Comp.firstorder_value [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Comp.hpp [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Comp.o [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Comp.oext [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Comp.o' [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Comp.o'ext [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.ExtEq [section, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.ExtEq.env [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.ExtEq.env' [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.ExtEq.eval [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.ExtEq.eval' [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.ExtEq.firstorder_value' [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.ExtEq.firstorder_value [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.ExtEq.o [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Opt [section, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Opt.compile_fo_value [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Opt.env [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Opt.env' [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Opt.eval [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Opt.eval' [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Opt.firstorder_value' [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Opt.firstorder_value [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.Opt.o [variable, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.preserves_fo [projection, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.proper_pres [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.t [record, in MetaRocq.ErasurePlugin.ErasureCorrectness]
ETransformPresFO.transform_fo [projection, in MetaRocq.ErasurePlugin.ErasureCorrectness]
et_view_other [constructor, in MetaRocq.Erasure.Typed.Erasure]
et_view_ind [constructor, in MetaRocq.Erasure.Typed.Erasure]
et_view_const [constructor, in MetaRocq.Erasure.Typed.Erasure]
et_view_app [constructor, in MetaRocq.Erasure.Typed.Erasure]
et_view_prod [constructor, in MetaRocq.Erasure.Typed.Erasure]
et_view_sort [constructor, in MetaRocq.Erasure.Typed.Erasure]
et_view_rel [constructor, in MetaRocq.Erasure.Typed.Erasure]
EUnboxing [library]
eval [inductive, in MetaRocq.Template.WcbvEval]
eval [abbreviation, in MetaRocq.Erasure.EWcbvEval]
eval [inductive, in MetaRocq.Erasure.EWcbvEval]
eval [inductive, in MetaRocq.Erasure.EWcbvEvalNamed]
eval [inductive, in MetaRocq.PCUIC.PCUICWcbvEval]
evalPrimArray [constructor, in MetaRocq.Erasure.EWcbvEval]
evalPrimArray [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
evalPrimArrayDep [constructor, in MetaRocq.Erasure.EWcbvEval]
evalPrimArrayDep [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
evalPrimFloat [constructor, in MetaRocq.Erasure.EWcbvEval]
evalPrimFloat [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
evalPrimFloatDep [constructor, in MetaRocq.Erasure.EWcbvEval]
evalPrimFloatDep [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
evalPrimInt [constructor, in MetaRocq.Erasure.EWcbvEval]
evalPrimInt [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
evalPrimIntDep [constructor, in MetaRocq.Erasure.EWcbvEval]
evalPrimIntDep [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
evalPrimString [constructor, in MetaRocq.Erasure.EWcbvEval]
evalPrimString [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
evalPrimStringDep [constructor, in MetaRocq.Erasure.EWcbvEval]
evalPrimStringDep [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
Evaluable [record, in MetaRocq.Common.Universes]
Evaluable [inductive, in MetaRocq.Common.Universes]
eval_template_program_env [definition, in MetaRocq.Template.TemplateProgram]
eval_template_program [definition, in MetaRocq.Template.TemplateProgram]
eval_global_deps [lemma, in MetaRocq.Erasure.ErasureFunction]
eval_inlined_program [definition, in MetaRocq.Erasure.EInlining]
eval_pcuic_quotation [record, in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
eval_pcuic_quotation [inductive, in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
eval_pcuic_quotation [abbreviation, in MetaRocq.TemplatePCUIC.Loader]
eval_proj_eval_inv_discr [lemma, in MetaRocq.Erasure.ErasureProperties]
eval_case_eval_inv_discr [lemma, in MetaRocq.Erasure.ErasureProperties]
eval_case_eval_discr [lemma, in MetaRocq.Erasure.ErasureProperties]
eval_case_tBox_inv [lemma, in MetaRocq.Erasure.ErasureProperties]
eval_empty_brs [lemma, in MetaRocq.Erasure.ErasureProperties]
eval_preserve_mkApps_ind [lemma, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd]
eval_beta_inv [lemma, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd]
eval_mkApps_cong [lemma, in MetaRocq.Template.WcbvEval]
eval_Const [lemma, in MetaRocq.Template.WcbvEval]
eval_LetIn [lemma, in MetaRocq.Template.WcbvEval]
eval_to_stuck_fix_inv [lemma, in MetaRocq.Template.WcbvEval]
eval_atom_inj [lemma, in MetaRocq.Template.WcbvEval]
eval_to_value [lemma, in MetaRocq.Template.WcbvEval]
eval_evals_ind [definition, in MetaRocq.Template.WcbvEval]
eval_sind [definition, in MetaRocq.Template.WcbvEval]
eval_rec [definition, in MetaRocq.Template.WcbvEval]
eval_ind [definition, in MetaRocq.Template.WcbvEval]
eval_rect [definition, in MetaRocq.Template.WcbvEval]
eval_atom [constructor, in MetaRocq.Template.WcbvEval]
eval_tArray [constructor, in MetaRocq.Template.WcbvEval]
eval_app_cong [constructor, in MetaRocq.Template.WcbvEval]
eval_construct [constructor, in MetaRocq.Template.WcbvEval]
eval_cofix_proj [constructor, in MetaRocq.Template.WcbvEval]
eval_cofix_case [constructor, in MetaRocq.Template.WcbvEval]
eval_fix_value [constructor, in MetaRocq.Template.WcbvEval]
eval_fix [constructor, in MetaRocq.Template.WcbvEval]
eval_proj [constructor, in MetaRocq.Template.WcbvEval]
eval_iota [constructor, in MetaRocq.Template.WcbvEval]
eval_delta [constructor, in MetaRocq.Template.WcbvEval]
eval_zeta [constructor, in MetaRocq.Template.WcbvEval]
eval_beta [constructor, in MetaRocq.Template.WcbvEval]
eval_mkApps_rect [lemma, in MetaRocq.Erasure.EWcbvEvalInd]
eval_mkApps_rect.IH [variable, in MetaRocq.Erasure.EWcbvEvalInd]
eval_mkApps_rect.P [variable, in MetaRocq.Erasure.EWcbvEvalInd]
eval_mkApps_rect.Σ [variable, in MetaRocq.Erasure.EWcbvEvalInd]
eval_mkApps_rect.wfl [variable, in MetaRocq.Erasure.EWcbvEvalInd]
eval_mkApps_rect [section, in MetaRocq.Erasure.EWcbvEvalInd]
eval_mkApps_heads_deriv [lemma, in MetaRocq.Erasure.Typed.WcbvEvalAux]
eval_tApp_heads_deriv [lemma, in MetaRocq.Erasure.Typed.WcbvEvalAux]
eval_mkApps_deriv [lemma, in MetaRocq.Erasure.Typed.WcbvEvalAux]
eval_tApp_deriv [lemma, in MetaRocq.Erasure.Typed.WcbvEvalAux]
eval_prim_length [definition, in MetaRocq.Erasure.Typed.WcbvEvalAux]
eval_mkApps_heads [lemma, in MetaRocq.Erasure.Typed.WcbvEvalAux]
eval_tApp_tLambda_inv [lemma, in MetaRocq.Erasure.Typed.WcbvEvalAux]
eval_tLambda_inv [lemma, in MetaRocq.Erasure.Typed.WcbvEvalAux]
eval_tLetIn_inv [lemma, in MetaRocq.Erasure.Typed.WcbvEvalAux]
eval_tApp_heads [lemma, in MetaRocq.Erasure.Typed.WcbvEvalAux]
eval_mkApps_args [lemma, in MetaRocq.Erasure.Typed.WcbvEvalAux]
eval_mkApps_head [lemma, in MetaRocq.Erasure.Typed.WcbvEvalAux]
eval_tApp_arg [lemma, in MetaRocq.Erasure.Typed.WcbvEvalAux]
eval_tApp_head [lemma, in MetaRocq.Erasure.Typed.WcbvEvalAux]
eval_wt [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
eval_etaexp [lemma, in MetaRocq.Erasure.EWcbvEvalEtaInd]
eval_preserve_mkApps_ind [lemma, in MetaRocq.Erasure.EWcbvEvalEtaInd]
eval_preserve_mkApps_ind [lemma, in MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksInd]
eval_wf [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
eval_mkApps_cong [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
eval_mkApps_fix [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
eval_mkApps_value_cong [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
eval_value_cong [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
eval_stuck_fix [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
eval_to_stuck_fix_inv [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
eval_mkApps [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
eval_tApp [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
eval_eval [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
eval_mkApps_inv [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
eval_eprogram_env [definition, in MetaRocq.Erasure.EProgram]
eval_eprogram [definition, in MetaRocq.Erasure.EProgram]
eval_opt_to_target [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
eval_app_cong_mkApps [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
eval_value_cong [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
eval_app_cong_tApp' [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
eval_stuck_fix_eq [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
eval_etaexp [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
eval_app_cong_tApp [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
eval_is_box [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
eval_mkApps_Construct_inv [lemma, in MetaRocq.Erasure.EConstructorsAsBlocks]
eval_tCase [lemma, in MetaRocq.PCUIC.PCUICProgress]
eval_eprogram_env_mapping [definition, in MetaRocq.ErasurePlugin.ETransform]
eval_eprogram_mapping [definition, in MetaRocq.ErasurePlugin.ETransform]
eval_typed_eprogram_masks [definition, in MetaRocq.ErasurePlugin.ETransform]
eval_typed_eprogram [definition, in MetaRocq.ErasurePlugin.ETransform]
eval_box_apps [lemma, in MetaRocq.Erasure.EWcbvEval]
eval_construct_size [lemma, in MetaRocq.Erasure.EWcbvEval]
eval_mkApps_Construct_size [lemma, in MetaRocq.Erasure.EWcbvEval]
eval_mkApps_inv_size [lemma, in MetaRocq.Erasure.EWcbvEval]
eval_mkApps_Construct_block_inv [lemma, in MetaRocq.Erasure.EWcbvEval]
eval_mkApps_Construct_inv [lemma, in MetaRocq.Erasure.EWcbvEval]
eval_mkApps_inv' [lemma, in MetaRocq.Erasure.EWcbvEval]
eval_mkApps_tFix_inv_size_unguarded [lemma, in MetaRocq.Erasure.EWcbvEval]
eval_to_values [lemma, in MetaRocq.Erasure.EWcbvEval]
eval_mkApps_tFix_inv_size [lemma, in MetaRocq.Erasure.EWcbvEval]
eval_wellformed [lemma, in MetaRocq.Erasure.EWcbvEval]
eval_closed [lemma, in MetaRocq.Erasure.EWcbvEval]
eval_nondep [definition, in MetaRocq.Erasure.EWcbvEval]
eval_mkApps_inv [lemma, in MetaRocq.Erasure.EWcbvEval]
eval_trans [lemma, in MetaRocq.Erasure.EWcbvEval]
eval_trans' [lemma, in MetaRocq.Erasure.EWcbvEval]
eval_deterministic_all [lemma, in MetaRocq.Erasure.EWcbvEval]
eval_value [lemma, in MetaRocq.Erasure.EWcbvEval]
eval_deterministic [lemma, in MetaRocq.Erasure.EWcbvEval]
eval_unique [lemma, in MetaRocq.Erasure.EWcbvEval]
eval_unique_sig [lemma, in MetaRocq.Erasure.EWcbvEval]
eval_mkApps_cong [lemma, in MetaRocq.Erasure.EWcbvEval]
eval_mkApps_tBox [lemma, in MetaRocq.Erasure.EWcbvEval]
eval_mkApps_CoFix [lemma, in MetaRocq.Erasure.EWcbvEval]
eval_mkApps_Construct_block [lemma, in MetaRocq.Erasure.EWcbvEval]
eval_mkApps_Construct [lemma, in MetaRocq.Erasure.EWcbvEval]
eval_stuck_Fix [lemma, in MetaRocq.Erasure.EWcbvEval]
eval_to_mkApps_tBox_inv [lemma, in MetaRocq.Erasure.EWcbvEval]
eval_mkApps_tFix_inv [lemma, in MetaRocq.Erasure.EWcbvEval]
eval_mkApps_tCoFix [lemma, in MetaRocq.Erasure.EWcbvEval]
eval_to_value [lemma, in MetaRocq.Erasure.EWcbvEval]
eval_Construct_inv [lemma, in MetaRocq.Erasure.EWcbvEval]
eval_ind [definition, in MetaRocq.Erasure.EWcbvEval]
eval_rec [definition, in MetaRocq.Erasure.EWcbvEval]
eval_rect [lemma, in MetaRocq.Erasure.EWcbvEval]
eval_rect.P [variable, in MetaRocq.Erasure.EWcbvEval]
eval_rect.Σ [variable, in MetaRocq.Erasure.EWcbvEval]
eval_rect.wfl [variable, in MetaRocq.Erasure.EWcbvEval]
eval_rect [section, in MetaRocq.Erasure.EWcbvEval]
eval_depth [definition, in MetaRocq.Erasure.EWcbvEval]
eval_primitive_depth [definition, in MetaRocq.Erasure.EWcbvEval]
eval_atom [constructor, in MetaRocq.Erasure.EWcbvEval]
eval_force [constructor, in MetaRocq.Erasure.EWcbvEval]
eval_prim [constructor, in MetaRocq.Erasure.EWcbvEval]
eval_app_cong [constructor, in MetaRocq.Erasure.EWcbvEval]
eval_construct_block [constructor, in MetaRocq.Erasure.EWcbvEval]
eval_construct [constructor, in MetaRocq.Erasure.EWcbvEval]
eval_proj_prop [constructor, in MetaRocq.Erasure.EWcbvEval]
eval_proj_block [constructor, in MetaRocq.Erasure.EWcbvEval]
eval_proj [constructor, in MetaRocq.Erasure.EWcbvEval]
eval_delta [constructor, in MetaRocq.Erasure.EWcbvEval]
eval_cofix_proj [constructor, in MetaRocq.Erasure.EWcbvEval]
eval_cofix_case [constructor, in MetaRocq.Erasure.EWcbvEval]
eval_fix' [constructor, in MetaRocq.Erasure.EWcbvEval]
eval_fix_value [constructor, in MetaRocq.Erasure.EWcbvEval]
eval_fix [constructor, in MetaRocq.Erasure.EWcbvEval]
eval_iota_sing [constructor, in MetaRocq.Erasure.EWcbvEval]
eval_iota_block [constructor, in MetaRocq.Erasure.EWcbvEval]
eval_iota [constructor, in MetaRocq.Erasure.EWcbvEval]
eval_zeta [constructor, in MetaRocq.Erasure.EWcbvEval]
eval_beta [constructor, in MetaRocq.Erasure.EWcbvEval]
eval_box [constructor, in MetaRocq.Erasure.EWcbvEval]
eval_primitive_ind [inductive, in MetaRocq.Erasure.EWcbvEval]
eval_primitive [inductive, in MetaRocq.Erasure.EWcbvEval]
eval_typed_eprogram_masks_mapping [definition, in MetaRocq.ErasurePlugin.Erasure]
eval_typed_eprogram_mapping [definition, in MetaRocq.ErasurePlugin.Erasure]
eval_template_program_env_mapping [definition, in MetaRocq.ErasurePlugin.Erasure]
eval_template_program_mapping [definition, in MetaRocq.ErasurePlugin.Erasure]
eval_pcuic_program_mapping [definition, in MetaRocq.ErasurePlugin.Erasure]
eval_to_eval_named_full [lemma, in MetaRocq.Erasure.EWcbvEvalNamed]
eval_to_eval_named [lemma, in MetaRocq.Erasure.EWcbvEvalNamed]
eval_construct_All2 [lemma, in MetaRocq.Erasure.EWcbvEvalNamed]
eval_wf [lemma, in MetaRocq.Erasure.EWcbvEvalNamed]
eval_represents_value [lemma, in MetaRocq.Erasure.EWcbvEvalNamed]
eval_ind [definition, in MetaRocq.Erasure.EWcbvEvalNamed]
eval_force [constructor, in MetaRocq.Erasure.EWcbvEvalNamed]
eval_lazy [constructor, in MetaRocq.Erasure.EWcbvEvalNamed]
eval_prim [constructor, in MetaRocq.Erasure.EWcbvEvalNamed]
eval_construct_block_empty [constructor, in MetaRocq.Erasure.EWcbvEvalNamed]
eval_construct_block [constructor, in MetaRocq.Erasure.EWcbvEvalNamed]
eval_delta [constructor, in MetaRocq.Erasure.EWcbvEvalNamed]
eval_fix [constructor, in MetaRocq.Erasure.EWcbvEvalNamed]
eval_fix_unfold [constructor, in MetaRocq.Erasure.EWcbvEvalNamed]
eval_iota_block [constructor, in MetaRocq.Erasure.EWcbvEvalNamed]
eval_zeta [constructor, in MetaRocq.Erasure.EWcbvEvalNamed]
eval_lambda [constructor, in MetaRocq.Erasure.EWcbvEvalNamed]
eval_beta [constructor, in MetaRocq.Erasure.EWcbvEvalNamed]
eval_var [constructor, in MetaRocq.Erasure.EWcbvEvalNamed]
eval_pcuic_quotation [abbreviation, in MetaRocq.TemplatePCUIC.PCUICTemplateMonad.Core]
eval_classification [lemma, in MetaRocq.PCUIC.PCUICClassification]
eval_whne [lemma, in MetaRocq.PCUIC.PCUICClassification]
eval_tCase [lemma, in MetaRocq.Erasure.EArities]
eval_const_construct_expanded [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
eval_debox_env_types [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
eval_mkApps_Construct_inv' [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
eval_mkApps_dearg_reduce [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
eval_mkApps_dearg [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
eval_tApp_dearg [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
eval_mkApps_tConstruct [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
eval_valid_cases [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
eval_is_expanded_aux [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
eval_dearg_lambdas_inv [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
eval_Const [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
eval_LetIn [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
eval_unique [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
eval_deterministic [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
eval_unique_sig [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
eval_mkApps_tCoFix [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
eval_tEvar [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
eval_tVar [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
eval_tRel [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
eval_closed [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
eval_stuck_fix [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
eval_mkApps_cong [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
eval_stuck_Fix [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
eval_mkApps_tInd [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
eval_mkApps_CoFix [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
eval_mkApps_Construct [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
eval_to_value [lemma, in MetaRocq.PCUIC.PCUICWcbvEval]
eval_ind [definition, in MetaRocq.PCUIC.PCUICWcbvEval]
eval_rect [definition, in MetaRocq.PCUIC.PCUICWcbvEval]
eval_atom [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
eval_prim [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
eval_app_cong [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
eval_construct [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
eval_cofix_proj [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
eval_cofix_case [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
eval_fix_value [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
eval_fix [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
eval_proj [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
eval_iota [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
eval_delta [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
eval_zeta [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
eval_beta [constructor, in MetaRocq.PCUIC.PCUICWcbvEval]
eval_primitive_ind [inductive, in MetaRocq.PCUIC.PCUICWcbvEval]
eval_primitive [inductive, in MetaRocq.PCUIC.PCUICWcbvEval]
eval_pcuic_program [definition, in MetaRocq.TemplatePCUIC.PCUICTransform]
eval_is_box [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
evar_pred [constructor, in MetaRocq.PCUIC.PCUICParallelReduction]
evar_red [constructor, in MetaRocq.Template.Typing]
evar_red [constructor, in MetaRocq.PCUIC.PCUICReduction]
even [definition, in MetaRocq.Examples.demo]
everything [constructor, in MetaRocq.Quotation.ToPCUIC.Init]
everything [constructor, in MetaRocq.Quotation.ToTemplate.Init]
EWcbvEval [library]
EWcbvEvalCstrsAsBlocksFixLambdaInd [library]
EWcbvEvalCstrsAsBlocksInd [library]
EWcbvEvalEtaInd [library]
EWcbvEvalInd [library]
EWcbvEvalNamed [library]
EWellformed [library]
EWtAst [library]
Ex [module, in MetaRocq.Erasure.Typed.Annotations]
Ex [module, in MetaRocq.Erasure.Typed.Erasure]
ExAst [library]
existsb_map [lemma, in MetaRocq.Erasure.Typed.Utils]
exists_neg_forall [lemma, in MetaRocq.Common.uGraph]
exist_irrel_eq [lemma, in MetaRocq.Erasure.EPrimitive]
exist_irrel_eq [lemma, in MetaRocq.PCUIC.utils.PCUICPrimitive]
expand [abbreviation, in MetaRocq.SafeChecker.PCUICSafeConversion]
expanded [inductive, in MetaRocq.Erasure.EEtaExpanded]
expanded [section, in MetaRocq.Erasure.EEtaExpanded]
expanded [inductive, in MetaRocq.Template.EtaExpand]
expanded [section, in MetaRocq.Template.EtaExpand]
expanded [inductive, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded [section, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded [inductive, in MetaRocq.Erasure.EEtaExpandedFix]
expanded [section, in MetaRocq.Erasure.EEtaExpandedFix]
ExpandedFix [section, in MetaRocq.Erasure.EOptimizePropDiscr]
expanded_erases [lemma, in MetaRocq.Erasure.ErasureCorrectness]
expanded_mkApps_expanded [lemma, in MetaRocq.Erasure.EEtaExpanded]
expanded_global_env_isEtaExp_env [lemma, in MetaRocq.Erasure.EEtaExpanded]
expanded_isEtaExp [lemma, in MetaRocq.Erasure.EEtaExpanded]
expanded_isEtaExp_app_ [lemma, in MetaRocq.Erasure.EEtaExpanded]
expanded_eprogram_env_cstrs [definition, in MetaRocq.Erasure.EEtaExpanded]
expanded_eprogram_cstrs [definition, in MetaRocq.Erasure.EEtaExpanded]
expanded_global_env [definition, in MetaRocq.Erasure.EEtaExpanded]
expanded_global_declarations_sind [definition, in MetaRocq.Erasure.EEtaExpanded]
expanded_global_declarations_ind [definition, in MetaRocq.Erasure.EEtaExpanded]
expanded_global_cons [constructor, in MetaRocq.Erasure.EEtaExpanded]
expanded_global_nil [constructor, in MetaRocq.Erasure.EEtaExpanded]
expanded_global_declarations [inductive, in MetaRocq.Erasure.EEtaExpanded]
expanded_decl [definition, in MetaRocq.Erasure.EEtaExpanded]
expanded_constant_decl [definition, in MetaRocq.Erasure.EEtaExpanded]
expanded_ind [lemma, in MetaRocq.Erasure.EEtaExpanded]
expanded_tBox [constructor, in MetaRocq.Erasure.EEtaExpanded]
expanded_tForce [constructor, in MetaRocq.Erasure.EEtaExpanded]
expanded_tLazy [constructor, in MetaRocq.Erasure.EEtaExpanded]
expanded_tPrim [constructor, in MetaRocq.Erasure.EEtaExpanded]
expanded_tConstruct_app [constructor, in MetaRocq.Erasure.EEtaExpanded]
expanded_tCoFix [constructor, in MetaRocq.Erasure.EEtaExpanded]
expanded_tFix [constructor, in MetaRocq.Erasure.EEtaExpanded]
expanded_tProj [constructor, in MetaRocq.Erasure.EEtaExpanded]
expanded_tCase [constructor, in MetaRocq.Erasure.EEtaExpanded]
expanded_tConst [constructor, in MetaRocq.Erasure.EEtaExpanded]
expanded_mkApps [constructor, in MetaRocq.Erasure.EEtaExpanded]
expanded_tLetIn [constructor, in MetaRocq.Erasure.EEtaExpanded]
expanded_tLambda [constructor, in MetaRocq.Erasure.EEtaExpanded]
expanded_tEvar [constructor, in MetaRocq.Erasure.EEtaExpanded]
expanded_tVar [constructor, in MetaRocq.Erasure.EEtaExpanded]
expanded_tRel [constructor, in MetaRocq.Erasure.EEtaExpanded]
expanded_erase_fast [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
expanded_erase_global_fast [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
expanded_erase_global [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
expanded_erase [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
expanded_weakening_global [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
expanded_decl_env_irrel [lemma, in MetaRocq.Template.EtaExpand]
expanded_context_env_irrel [lemma, in MetaRocq.Template.EtaExpand]
expanded_env_irrel [lemma, in MetaRocq.Template.EtaExpand]
expanded_eta_single_tRel_app [lemma, in MetaRocq.Template.EtaExpand]
expanded_lift' [lemma, in MetaRocq.Template.EtaExpand]
expanded_lift [lemma, in MetaRocq.Template.EtaExpand]
expanded_unlift [lemma, in MetaRocq.Template.EtaExpand]
expanded_mkApps [lemma, in MetaRocq.Template.EtaExpand]
expanded_mkApps_inv [lemma, in MetaRocq.Template.EtaExpand]
expanded_tApps_inv [lemma, in MetaRocq.Template.EtaExpand]
expanded_tApp_args [lemma, in MetaRocq.Template.EtaExpand]
expanded_mkApps_tFix_inv [lemma, in MetaRocq.Template.EtaExpand]
expanded_mkApps_tFix [lemma, in MetaRocq.Template.EtaExpand]
expanded_mkApps_tConstruct [lemma, in MetaRocq.Template.EtaExpand]
expanded_fold_lambda [lemma, in MetaRocq.Template.EtaExpand]
expanded_program [definition, in MetaRocq.Template.EtaExpand]
expanded_global_env [definition, in MetaRocq.Template.EtaExpand]
expanded_global_declarations_sind [definition, in MetaRocq.Template.EtaExpand]
expanded_global_declarations_ind [definition, in MetaRocq.Template.EtaExpand]
expanded_global_cons [constructor, in MetaRocq.Template.EtaExpand]
expanded_global_nil [constructor, in MetaRocq.Template.EtaExpand]
expanded_global_declarations [inductive, in MetaRocq.Template.EtaExpand]
expanded_decl [definition, in MetaRocq.Template.EtaExpand]
expanded_ind_bodies [projection, in MetaRocq.Template.EtaExpand]
expanded_params [projection, in MetaRocq.Template.EtaExpand]
expanded_minductive_decl [record, in MetaRocq.Template.EtaExpand]
expanded_ind_ctors [projection, in MetaRocq.Template.EtaExpand]
expanded_inductive_decl [record, in MetaRocq.Template.EtaExpand]
expanded_cstr_type [projection, in MetaRocq.Template.EtaExpand]
expanded_cstr_args [projection, in MetaRocq.Template.EtaExpand]
expanded_constructor_decl [record, in MetaRocq.Template.EtaExpand]
expanded_context [definition, in MetaRocq.Template.EtaExpand]
expanded_body [projection, in MetaRocq.Template.EtaExpand]
expanded_constant_decl [record, in MetaRocq.Template.EtaExpand]
expanded_ind [lemma, in MetaRocq.Template.EtaExpand]
expanded_tArray [constructor, in MetaRocq.Template.EtaExpand]
expanded_tString [constructor, in MetaRocq.Template.EtaExpand]
expanded_tFloat [constructor, in MetaRocq.Template.EtaExpand]
expanded_tInt [constructor, in MetaRocq.Template.EtaExpand]
expanded_tConstruct_app [constructor, in MetaRocq.Template.EtaExpand]
expanded_tCoFix [constructor, in MetaRocq.Template.EtaExpand]
expanded_tFix [constructor, in MetaRocq.Template.EtaExpand]
expanded_tProj [constructor, in MetaRocq.Template.EtaExpand]
expanded_tCase [constructor, in MetaRocq.Template.EtaExpand]
expanded_tConstruct [constructor, in MetaRocq.Template.EtaExpand]
expanded_tInd [constructor, in MetaRocq.Template.EtaExpand]
expanded_tConst [constructor, in MetaRocq.Template.EtaExpand]
expanded_tApp [constructor, in MetaRocq.Template.EtaExpand]
expanded_tLetIn [constructor, in MetaRocq.Template.EtaExpand]
expanded_tLambda [constructor, in MetaRocq.Template.EtaExpand]
expanded_tProd [constructor, in MetaRocq.Template.EtaExpand]
expanded_tCast [constructor, in MetaRocq.Template.EtaExpand]
expanded_tSort [constructor, in MetaRocq.Template.EtaExpand]
expanded_tEvar [constructor, in MetaRocq.Template.EtaExpand]
expanded_tVar [constructor, in MetaRocq.Template.EtaExpand]
expanded_tRel_app [constructor, in MetaRocq.Template.EtaExpand]
expanded_tRel [constructor, in MetaRocq.Template.EtaExpand]
expanded_expand_lets_program [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expanded_global_env_expand_lets [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expanded_smash_context [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expanded_trans_local [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expanded_expand_lets [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expanded_tApp_arg [lemma, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_red [lemma, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_red1 [lemma, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_global_env_constant [lemma, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_weakening_env [lemma, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_unfold_cofix [lemma, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_unfold_fix [lemma, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_fix_subst [lemma, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_mkApps_inv' [lemma, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_mkApps_inv [lemma, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_tPrim_inv [lemma, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_tCoFix_inv [lemma, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_tProj_inv [lemma, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_tCase_inv [lemma, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_tEvar_inv [lemma, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_tLetIn_inv [lemma, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_tLambda_inv [lemma, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_tApp_inv [lemma, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_tApp [lemma, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_weakening [lemma, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_subst_instance [lemma, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_let_expansion [lemma, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_subst [lemma, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_lift [lemma, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_mkApps_expanded [lemma, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_pcuic_program [definition, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_global_env [definition, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_global_declarations_sind [definition, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_global_declarations_ind [definition, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_global_cons [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_global_nil [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_global_declarations [inductive, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_decl [definition, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_ind_bodies [projection, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_params [projection, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_minductive_decl [record, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_ind_ctors [projection, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_inductive_decl [record, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_cstr_args [projection, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_constructor_decl [record, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_body [projection, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_constant_decl [record, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_ind [lemma, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_context [definition, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_tPrim [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_tConstruct_app [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_tCoFix [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_tFix [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_tProj [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_tCase [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_tInd [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_tConst [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_mkApps [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_tLetIn [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_tLambda [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_tProd [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_tSort [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_tEvar [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_tVar [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_tRel [constructor, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_global_env_isEtaExp_env [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
expanded_isEtaExp [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
expanded_isEtaExp_app_ [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
expanded_weakening [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
expanded_head_viewc [definition, in MetaRocq.Erasure.EEtaExpandedFix]
expanded_head_view_sind [definition, in MetaRocq.Erasure.EEtaExpandedFix]
expanded_head_view_rec [definition, in MetaRocq.Erasure.EEtaExpandedFix]
expanded_head_view_ind [definition, in MetaRocq.Erasure.EEtaExpandedFix]
expanded_head_view_rect [definition, in MetaRocq.Erasure.EEtaExpandedFix]
expanded_head_other [constructor, in MetaRocq.Erasure.EEtaExpandedFix]
expanded_head_rel [constructor, in MetaRocq.Erasure.EEtaExpandedFix]
expanded_head_fix [constructor, in MetaRocq.Erasure.EEtaExpandedFix]
expanded_head_construct [constructor, in MetaRocq.Erasure.EEtaExpandedFix]
expanded_head_view [inductive, in MetaRocq.Erasure.EEtaExpandedFix]
expanded_closed [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
expanded_eprogram_env [definition, in MetaRocq.Erasure.EEtaExpandedFix]
expanded_eprogram [definition, in MetaRocq.Erasure.EEtaExpandedFix]
expanded_global_env [definition, in MetaRocq.Erasure.EEtaExpandedFix]
expanded_global_declarations_sind [definition, in MetaRocq.Erasure.EEtaExpandedFix]
expanded_global_declarations_ind [definition, in MetaRocq.Erasure.EEtaExpandedFix]
expanded_global_cons [constructor, in MetaRocq.Erasure.EEtaExpandedFix]
expanded_global_nil [constructor, in MetaRocq.Erasure.EEtaExpandedFix]
expanded_global_declarations [inductive, in MetaRocq.Erasure.EEtaExpandedFix]
expanded_decl [definition, in MetaRocq.Erasure.EEtaExpandedFix]
expanded_constant_decl [definition, in MetaRocq.Erasure.EEtaExpandedFix]
expanded_ind [lemma, in MetaRocq.Erasure.EEtaExpandedFix]
expanded_tBox [constructor, in MetaRocq.Erasure.EEtaExpandedFix]
expanded_tForce [constructor, in MetaRocq.Erasure.EEtaExpandedFix]
expanded_tLazy [constructor, in MetaRocq.Erasure.EEtaExpandedFix]
expanded_tPrim [constructor, in MetaRocq.Erasure.EEtaExpandedFix]
expanded_tConstruct_app [constructor, in MetaRocq.Erasure.EEtaExpandedFix]
expanded_tCoFix [constructor, in MetaRocq.Erasure.EEtaExpandedFix]
expanded_tFix [constructor, in MetaRocq.Erasure.EEtaExpandedFix]
expanded_tProj [constructor, in MetaRocq.Erasure.EEtaExpandedFix]
expanded_tCase [constructor, in MetaRocq.Erasure.EEtaExpandedFix]
expanded_tConst [constructor, in MetaRocq.Erasure.EEtaExpandedFix]
expanded_mkApps [constructor, in MetaRocq.Erasure.EEtaExpandedFix]
expanded_tLetIn [constructor, in MetaRocq.Erasure.EEtaExpandedFix]
expanded_tLambda [constructor, in MetaRocq.Erasure.EEtaExpandedFix]
expanded_tEvar [constructor, in MetaRocq.Erasure.EEtaExpandedFix]
expanded_tVar [constructor, in MetaRocq.Erasure.EEtaExpandedFix]
expanded_tRel_app [constructor, in MetaRocq.Erasure.EEtaExpandedFix]
expanded_erase_global_decls_recursive [lemma, in MetaRocq.Erasure.Typed.ExtractionCorrectness]
expanded_erase_global_decl [lemma, in MetaRocq.Erasure.Typed.ExtractionCorrectness]
expanded_erase [lemma, in MetaRocq.Erasure.Typed.ExtractionCorrectness]
expanded_mkApps_expanded [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
expanded_eprogram_env_expanded_eprogram_cstrs [lemma, in MetaRocq.ErasurePlugin.ETransform]
expanded_erase_program [lemma, in MetaRocq.ErasurePlugin.ETransform]
expanded_dearg_env [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
expanded_dearg [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
expanded_dearg_aux [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
expanded_trans_program [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICExpanded]
expanded_trans_global_env [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICExpanded]
expanded_trans_local [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICExpanded]
expanded_bcontext [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICExpanded]
expanded_context_weakening [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICExpanded]
expanded_weakening [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICExpanded]
expanded_inds [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICExpanded]
expanded_context_subst [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICExpanded]
expanded_let_expansion [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICExpanded]
expanded_extended_subst [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICExpanded]
expanded_context_map2_bias_left [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICExpanded]
expanded.Σ [variable, in MetaRocq.Erasure.EEtaExpanded]
expanded.Σ [variable, in MetaRocq.Template.EtaExpand]
expanded.Σ [variable, in MetaRocq.PCUIC.PCUICEtaExpand]
expanded.Σ [variable, in MetaRocq.Erasure.EEtaExpandedFix]
expand_lets_lift_cancel [lemma, in MetaRocq.PCUIC.PCUICSR]
expand_lets_eq_map [lemma, in MetaRocq.PCUIC.PCUICSR]
expand_lets_eq [lemma, in MetaRocq.PCUIC.PCUICSR]
expand_lets_erasure [lemma, in MetaRocq.Erasure.Prelim]
expand_lets_k_nil [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
expand_lets_subst_comm' [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
expand_lets_k_ctx_subst_id' [lemma, in MetaRocq.PCUIC.PCUICSpine]
expand_lets_ctx_o_lets [lemma, in MetaRocq.PCUIC.PCUICSpine]
expand_lets_eq [lemma, in MetaRocq.Template.TermEquality]
expand_lets_program [definition, in MetaRocq.PCUIC.PCUICExpandLets]
expand_firstorder_type [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_preserves_fo [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_inst_case_context [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_k_rel_ge [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_k_rel_lt [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_ctx_fix_context [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_k_ctx_fix_context [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_tCoFix [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_tFix [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_k_tRel_ass [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_fo [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_sound [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_expand_lets [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_smash_context_id [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_ctx_lift_context_cancel [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_comm [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_k_lift [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_set_binder_name [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_k_subst_comm [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_subst_comm [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_app [lemma, in MetaRocq.PCUIC.PCUICConversion]
expand_lets_k_app [lemma, in MetaRocq.PCUIC.PCUICConversion]
expand_lets_transform_env [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
expand_lets_eta_app [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
expand_lets_function [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
expand_lets_ctx_nil [lemma, in MetaRocq.PCUIC.PCUICContexts]
expand_lets_k_ctx_nil [lemma, in MetaRocq.PCUIC.PCUICContexts]
expand_lets_smash_context [lemma, in MetaRocq.PCUIC.PCUICContexts]
expand_lets_subst_comm [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
expand_lets_ctx_assumption_context [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
expand_lets_assumption_context [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
expand_lets_k_assumption_context [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
expand_lets_tRel [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
expand_lets_mkApps [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
expand_lets_k_mkApps [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
expand_lets_it_mkProd_or_LetIn [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
expand_lets_nil [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
expand_lets_k_ctx_decl [definition, in MetaRocq.PCUIC.PCUICSigmaCalculus]
expand_lets_k_ctx_vass [definition, in MetaRocq.PCUIC.PCUICSigmaCalculus]
expand_lets_vdef [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
expand_lets_k_vdef [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
expand_lets_vass [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
expand_lets_k_vass [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
expand_lets_ctx_app [lemma, in MetaRocq.PCUIC.PCUICInductives]
expand_lets_k_0 [lemma, in MetaRocq.PCUIC.PCUICInductives]
expand_lets_k_to_extended_list_k [lemma, in MetaRocq.PCUIC.PCUICInductives]
expand_lets_k_subst_comm [lemma, in MetaRocq.PCUIC.PCUICInductives]
expand_lets_ctx_tip [lemma, in MetaRocq.PCUIC.PCUICInductives]
expand_lets_ctx_snoc [lemma, in MetaRocq.PCUIC.PCUICInductives]
expand_lets_k_ctx_snoc [lemma, in MetaRocq.PCUIC.PCUICInductives]
expand_lets_ctx_lift [lemma, in MetaRocq.PCUIC.PCUICInductives]
expand_lets_lift [lemma, in MetaRocq.PCUIC.PCUICInductives]
expand_lets_subst_instance [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
export [constructor, in MetaRocq.Template.TemplateMonad.Common]
expr_set_forall_map [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
expr_gc_declared_declared [lemma, in MetaRocq.Common.uGraph]
extended_subst_app [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
extended_subst_set_binder_name [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
extended_subst_to_extended_list_k [lemma, in MetaRocq.PCUIC.PCUICContexts]
extended_subst_lift_context [lemma, in MetaRocq.PCUIC.PCUICInductives]
extended_subst_shiftn_impl [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
extended_subst_shiftn_aboveP [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
extended_subst_shiftn [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
extendP [definition, in MetaRocq.PCUIC.PCUICParallelReduction]
extends [definition, in MetaRocq.Erasure.EGlobalEnv]
ExtendsWf [section, in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
ExtendsWf [section, in MetaRocq.PCUIC.PCUICWeakeningEnv]
ExtendsWf.cf [variable, in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
ExtendsWf.cf [variable, in MetaRocq.PCUIC.PCUICWeakeningEnv]
ExtendsWf.P [variable, in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
ExtendsWf.P [variable, in MetaRocq.PCUIC.PCUICWeakeningEnv]
ExtendsWf.Pcmp [variable, in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
ExtendsWf.Pcmp [variable, in MetaRocq.PCUIC.PCUICWeakeningEnv]
ExtendsWf.wf [variable, in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
ExtendsWf.wf [variable, in MetaRocq.PCUIC.PCUICWeakeningEnv]
extends_global_env [definition, in MetaRocq.Erasure.ErasureFunction]
extends_inlined_eprogram [definition, in MetaRocq.Erasure.EInlining]
extends_lookup [lemma, in MetaRocq.PCUIC.PCUICWeakeningEnv]
extends_wf_sort [lemma, in MetaRocq.PCUIC.PCUICWeakeningEnv]
extends_wf_universe [lemma, in MetaRocq.PCUIC.PCUICWeakeningEnv]
extends_global_env_equiv_env [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
extends_filter [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
extends_filter_impl [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
extends_fresh [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
extends_cons [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
extends_decls_trans [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
extends_trans [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
extends_strictly_on_decls_trans [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
extends_cons_wf [lemma, in MetaRocq.Erasure.EGenericGlobalMap]
extends_cons_inv [lemma, in MetaRocq.Erasure.EGenericGlobalMap]
extends_prefix_extends [lemma, in MetaRocq.Erasure.EExtends]
extends_wf_glob [lemma, in MetaRocq.Erasure.EExtends]
extends_eq [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
extends_erase_pcuic_program [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
extends_eprogram_env [definition, in MetaRocq.Erasure.EProgram]
extends_eprogram [definition, in MetaRocq.Erasure.EProgram]
extends_cons_right [lemma, in MetaRocq.Erasure.Typed.ExtractionCorrectness]
extends_trans [lemma, in MetaRocq.Erasure.Typed.ExtractionCorrectness]
extends_inductive_isprop_and_pars [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
extends_cons_wf [lemma, in MetaRocq.Erasure.EGenericMapEnv]
extends_cons_inv [lemma, in MetaRocq.Erasure.EGenericMapEnv]
extends_lookup_projection [lemma, in MetaRocq.Erasure.EGenericMapEnv]
extends_lookup_projection [lemma, in MetaRocq.Erasure.EReorderCstrs]
extends_pcuic_program [definition, in MetaRocq.ErasurePlugin.ETransform]
extends_global_env [definition, in MetaRocq.ErasurePlugin.ETransform]
extends_fresh [lemma, in MetaRocq.Erasure.EWellformed]
extends_wf_global_decl [lemma, in MetaRocq.Erasure.EWellformed]
extends_wellformed [lemma, in MetaRocq.Erasure.EWellformed]
extends_is_propositional [lemma, in MetaRocq.Erasure.EWellformed]
extends_constructor_isprop_pars_decl [lemma, in MetaRocq.Erasure.EWellformed]
extends_lookup_constructor [lemma, in MetaRocq.Erasure.EWellformed]
extends_lookup_inductive [lemma, in MetaRocq.Erasure.EWellformed]
extends_lookup [lemma, in MetaRocq.Erasure.EWellformed]
extends_lookup_projection [lemma, in MetaRocq.Erasure.EInlineProjections]
extends_prefix [definition, in MetaRocq.Erasure.EGlobalEnv]
extends_lookup_inductive_pars [lemma, in MetaRocq.Erasure.ERemoveParams]
extends_trans_global_decls_acc [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
extends_primitive_constant [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
extends_wf_cofixpoint [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
extends_wf_fixpoint [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
extends_check_recursivity_kind [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
extends_strictly_on_decls_wf_local [definition, in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
extends_decls_wf_local [definition, in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
extends_wf_local [definition, in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
extends_wf_local_gen [lemma, in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
extends_lookup_inductive_kind [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
extends_inductive_isprop_and_pars [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
extend_over [definition, in MetaRocq.PCUIC.PCUICParallelReduction]
Extract [library]
Extractable [library]
ExtractableLoader [library]
Extraction [library]
Extraction [library]
Extraction [library]
Extraction [library]
ExtractionCorrectness [library]
extraction_checker_flags [instance, in MetaRocq.Common.config]
extraction_normalizing [instance, in MetaRocq.PCUIC.PCUICSN]
extraction_wcbv_flags [definition, in MetaRocq.Erasure.EWcbvEvalNamed]
extraction_env_flags [definition, in MetaRocq.Erasure.EWcbvEvalNamed]
extraction_term_flags [definition, in MetaRocq.Erasure.EWcbvEvalNamed]
ExtractTransform [definition, in MetaRocq.Erasure.Typed.Transform]
ExtractTransformCorrect [definition, in MetaRocq.Erasure.Typed.Transform]
extract_form [definition, in MetaRocq.Examples.tauto]
extract_template_env_within_coq [definition, in MetaRocq.Erasure.Typed.Extraction]
extract_within_coq [definition, in MetaRocq.Erasure.Typed.Extraction]
extract_template_env_certifying_passes [definition, in MetaRocq.Erasure.Typed.Extraction]
extract_template_env [definition, in MetaRocq.Erasure.Typed.Extraction]
extract_template_env_general [definition, in MetaRocq.Erasure.Typed.Extraction]
extract_template_env_params [record, in MetaRocq.Erasure.Typed.Extraction]
extract_pcuic_env [definition, in MetaRocq.Erasure.Typed.Extraction]
extract_transforms [projection, in MetaRocq.Erasure.Typed.Extraction]
extract_pcuic_params [record, in MetaRocq.Erasure.Typed.Extraction]
extract_def_name [definition, in MetaRocq.Erasure.Typed.Utils]
extract_def_name [definition, in MetaRocq.Erasure.Typed.CertifyingEta]
extract_def_name [definition, in MetaRocq.Erasure.Typed.CertifyingBeta]
extract_correct_gen' [lemma, in MetaRocq.Erasure.Typed.ExtractionCorrectness]
extract_correct_gen [lemma, in MetaRocq.Erasure.Typed.ExtractionCorrectness]
extract_correct [lemma, in MetaRocq.Erasure.Typed.ExtractionCorrectness]
extract_def_name [definition, in MetaRocq.Erasure.Typed.CertifyingInlining]
ext_lift [lemma, in MetaRocq.Template.EtaExpand]
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (19204 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (228 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (298 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1273 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (313 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (8163 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1514 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (52 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (352 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (534 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (727 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (402 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (333 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4833 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (182 entries) |