| 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 (definition)
Edecompose_app_annot [in MetaRocq.Erasure.Typed.Annotations]Edecompose_lam_annot [in MetaRocq.Erasure.Typed.Annotations]
EdgeSet_triple [in MetaRocq.Common.uGraph]
EdgeSet_pair [in MetaRocq.Common.uGraph]
edge_of_constraint [in MetaRocq.Common.uGraph]
edge_of_level [in MetaRocq.Common.uGraph]
emax [in MetaRocq.Common.BasicAst]
empty_trans_env [in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
empty_ext [in MetaRocq.PCUIC.utils.PCUICAstUtils]
EnvCheck_sind [in MetaRocq.SafeChecker.PCUICErrors]
EnvCheck_rec [in MetaRocq.SafeChecker.PCUICErrors]
EnvCheck_ind [in MetaRocq.SafeChecker.PCUICErrors]
EnvCheck_rect [in MetaRocq.SafeChecker.PCUICErrors]
EnvCheck_wf_env_ext [in MetaRocq.SafeCheckerPlugin.SafeTemplateChecker]
EnvCheck_X_env_ext_type [in MetaRocq.SafeChecker.PCUICSafeChecker]
EnvCheck_sind [in MetaRocq.Template.Checker]
EnvCheck_rec [in MetaRocq.Template.Checker]
EnvCheck_ind [in MetaRocq.Template.Checker]
EnvCheck_rect [in MetaRocq.Template.Checker]
environment [in MetaRocq.Erasure.EWcbvEvalNamed]
EnvironmentReflect.compatibleb [in MetaRocq.Common.EnvironmentReflect]
EnvironmentReflect.compatible_globalsb [in MetaRocq.Common.EnvironmentReflect]
EnvironmentReflect.extendsb [in MetaRocq.Common.EnvironmentReflect]
EnvironmentReflect.extends_strictly_on_declsb [in MetaRocq.Common.EnvironmentReflect]
EnvironmentReflect.extends_declsb [in MetaRocq.Common.EnvironmentReflect]
EnvironmentReflect.strictly_extends_declsb [in MetaRocq.Common.EnvironmentReflect]
Environment.add_global_decl [in MetaRocq.Common.Environment]
Environment.All_decls_alpha_sind [in MetaRocq.Common.Environment]
Environment.All_decls_alpha_rec [in MetaRocq.Common.Environment]
Environment.All_decls_alpha_ind [in MetaRocq.Common.Environment]
Environment.All_decls_alpha_rect [in MetaRocq.Common.Environment]
Environment.All_decls_sind [in MetaRocq.Common.Environment]
Environment.All_decls_rec [in MetaRocq.Common.Environment]
Environment.All_decls_ind [in MetaRocq.Common.Environment]
Environment.All_decls_rect [in MetaRocq.Common.Environment]
Environment.All2_fold_over [in MetaRocq.Common.Environment]
Environment.arities_context [in MetaRocq.Common.Environment]
Environment.array_uctx [in MetaRocq.Common.Environment]
Environment.compatible [in MetaRocq.Common.Environment]
Environment.compatible_globals [in MetaRocq.Common.Environment]
Environment.context [in MetaRocq.Common.Environment]
Environment.context_assumptions [in MetaRocq.Common.Environment]
Environment.declared_kername_set [in MetaRocq.Common.Environment]
Environment.empty_ext [in MetaRocq.Common.Environment]
Environment.empty_global_env [in MetaRocq.Common.Environment]
Environment.expand_lets_ctx [in MetaRocq.Common.Environment]
Environment.expand_lets_k_ctx [in MetaRocq.Common.Environment]
Environment.expand_lets [in MetaRocq.Common.Environment]
Environment.expand_lets_k [in MetaRocq.Common.Environment]
Environment.extended_subst [in MetaRocq.Common.Environment]
Environment.extends [in MetaRocq.Common.Environment]
Environment.extends_strictly_on_decls [in MetaRocq.Common.Environment]
Environment.extends_decls [in MetaRocq.Common.Environment]
Environment.fix_context [in MetaRocq.Common.Environment]
Environment.fst_ctx [in MetaRocq.Common.Environment]
Environment.global_env_ext [in MetaRocq.Common.Environment]
Environment.global_declarations [in MetaRocq.Common.Environment]
Environment.global_decl_sind [in MetaRocq.Common.Environment]
Environment.global_decl_rec [in MetaRocq.Common.Environment]
Environment.global_decl_ind [in MetaRocq.Common.Environment]
Environment.global_decl_rect [in MetaRocq.Common.Environment]
Environment.is_assumption_context [in MetaRocq.Common.Environment]
Environment.it_mkProd_or_LetIn [in MetaRocq.Common.Environment]
Environment.it_mkLambda_or_LetIn [in MetaRocq.Common.Environment]
Environment.judgment [in MetaRocq.Common.Environment]
Environment.lift_context [in MetaRocq.Common.Environment]
Environment.lift_decl [in MetaRocq.Common.Environment]
Environment.lookup_envs [in MetaRocq.Common.Environment]
Environment.lookup_globals [in MetaRocq.Common.Environment]
Environment.lookup_env [in MetaRocq.Common.Environment]
Environment.lookup_global [in MetaRocq.Common.Environment]
Environment.map_mutual_inductive_body [in MetaRocq.Common.Environment]
Environment.map_constant_body [in MetaRocq.Common.Environment]
Environment.map_one_inductive_body [in MetaRocq.Common.Environment]
Environment.map_projection_body [in MetaRocq.Common.Environment]
Environment.map_constructor_body [in MetaRocq.Common.Environment]
Environment.merge_global_envs [in MetaRocq.Common.Environment]
Environment.merge_globals [in MetaRocq.Common.Environment]
Environment.mkLambda_or_LetIn [in MetaRocq.Common.Environment]
Environment.mkProd_or_LetIn [in MetaRocq.Common.Environment]
Environment.primitive_invariants [in MetaRocq.Common.Environment]
Environment.primitive_constant [in MetaRocq.Common.Environment]
Environment.program [in MetaRocq.Common.Environment]
Environment.projs [in MetaRocq.Common.Environment]
Environment.reln [in MetaRocq.Common.Environment]
Environment.reln_alt [in MetaRocq.Common.Environment]
Environment.set_declarations [in MetaRocq.Common.Environment]
Environment.set_binder_name [in MetaRocq.Common.Environment]
Environment.smash_context [in MetaRocq.Common.Environment]
Environment.strictly_extends_decls [in MetaRocq.Common.Environment]
Environment.subst_telescope [in MetaRocq.Common.Environment]
Environment.subst_decl [in MetaRocq.Common.Environment]
Environment.subst_context [in MetaRocq.Common.Environment]
Environment.tImpl [in MetaRocq.Common.Environment]
Environment.to_extended_list [in MetaRocq.Common.Environment]
Environment.to_extended_list_k [in MetaRocq.Common.Environment]
Environment.vass [in MetaRocq.Common.Environment]
Environment.vdef [in MetaRocq.Common.Environment]
EnvMap.add [in MetaRocq.Common.EnvMap]
EnvMap.empty [in MetaRocq.Common.EnvMap]
EnvMap.equal [in MetaRocq.Common.EnvMap]
EnvMap.fresh_globals_sind [in MetaRocq.Common.EnvMap]
EnvMap.fresh_globals_ind [in MetaRocq.Common.EnvMap]
EnvMap.fresh_global [in MetaRocq.Common.EnvMap]
EnvMap.lookup [in MetaRocq.Common.EnvMap]
EnvMap.lookup_global [in MetaRocq.Common.EnvMap]
EnvMap.of_global_env [in MetaRocq.Common.EnvMap]
EnvMap.remove [in MetaRocq.Common.EnvMap]
EnvMap.repr [in MetaRocq.Common.EnvMap]
EnvMap.t [in MetaRocq.Common.EnvMap]
EnvTyping.All_local_rel_sorting_size [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_sorting_size [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_rel_size [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_size [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_size_gen [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_over [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_over_sorting_sind [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_over_sorting_rec [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_over_sorting_ind [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_over_sorting_rect [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_app_inv [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_rel_ind1 [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_rel_tip [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_rel_def [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_rel_abs [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_rel_snoc [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_rel_nil [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_rel [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_snoc [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_sind [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_rec [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_ind [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.All_local_env_rect [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.ctx_inst_sind [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.ctx_inst_rec [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.ctx_inst_ind [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.ctx_inst_rect [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_sorting_size_gen [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_sorting_extract [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_typing_conj [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_typing0 [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_sorting [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_wfbu_term [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_wfb_term [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_wfu_term [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.lift_wf_term [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.localenv_cons [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.on_def_body_size_gen [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.on_def_type_size_gen [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.on_wf_local_decl [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.on_def_body [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.on_def_type [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.option_default_size [in MetaRocq.Common.EnvironmentTyping]
EnvTyping.unlift_TypUniv [in MetaRocq.Common.EnvironmentTyping]
env_annots [in MetaRocq.Erasure.Typed.Annotations]
env_prop_bd [in MetaRocq.PCUIC.Bidirectional.BDTyping]
env_closed [in MetaRocq.Erasure.Typed.ClosedAux]
env_prop [in MetaRocq.PCUIC.PCUICTyping]
env_error_sind [in MetaRocq.SafeChecker.PCUICErrors]
env_error_rec [in MetaRocq.SafeChecker.PCUICErrors]
env_error_ind [in MetaRocq.SafeChecker.PCUICErrors]
env_error_rect [in MetaRocq.SafeChecker.PCUICErrors]
env_flags [in MetaRocq.Erasure.EWcbvEvalEtaInd]
env_prop [in MetaRocq.Template.Typing]
env_error_sind [in MetaRocq.Template.Checker]
env_error_rec [in MetaRocq.Template.Checker]
env_error_ind [in MetaRocq.Template.Checker]
env_error_rect [in MetaRocq.Template.Checker]
eprogram [in MetaRocq.Erasure.EProgram]
eprogram_env [in MetaRocq.Erasure.EProgram]
eqb [in MetaRocq.Utils.ByteCompare]
eqb_compare [in MetaRocq.Utils.ByteCompareSpec]
eqb_global_decl [in MetaRocq.Erasure.EReflect]
eqb_mutual_inductive_body [in MetaRocq.Erasure.EReflect]
eqb_one_inductive_body [in MetaRocq.Erasure.EReflect]
eqb_projection_body [in MetaRocq.Erasure.EReflect]
eqb_constructor_body [in MetaRocq.Erasure.EReflect]
eqb_constant_body [in MetaRocq.Erasure.EReflect]
eqb_sort_ [in MetaRocq.Common.Universes]
eqb_term [in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_termp [in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_termp_napp [in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_ctx [in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_ctx_gen_proper [in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_ctx_upto [in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_decl_gen [in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_term_upto_univ_proper [in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_univ_reflect [in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_term_upto_univ_napp [in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_decl_upto_names [in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_binder_annots [in MetaRocq.SafeChecker.PCUICEqualityDec]
eqb_Variance [in MetaRocq.Common.Reflect]
eqb_allowed_eliminations [in MetaRocq.Common.Reflect]
eqb_sorts_decl [in MetaRocq.Common.Reflect]
eqb_ConstraintType [in MetaRocq.Common.Reflect]
eqb_recursivity_kind [in MetaRocq.Common.Reflect]
eqb_context_decl [in MetaRocq.Common.Reflect]
eqb_case_info [in MetaRocq.Common.Reflect]
eqb_of_listable [in MetaRocq.Utils.MRListable]
eqb_binder_annot [in MetaRocq.Common.BasicAst]
eqb_predicate [in MetaRocq.PCUIC.PCUICAst]
eqb_predicate_gen [in MetaRocq.PCUIC.PCUICAst]
eqb_global_decl [in MetaRocq.Template.ReflectAst]
eqb_mutual_inductive_body [in MetaRocq.Template.ReflectAst]
eqb_one_inductive_body [in MetaRocq.Template.ReflectAst]
eqb_projection_body [in MetaRocq.Template.ReflectAst]
eqb_constructor_body [in MetaRocq.Template.ReflectAst]
eqb_constant_body [in MetaRocq.Template.ReflectAst]
eqb_universe_instance [in MetaRocq.SafeChecker.PCUICSafeConversion]
eqb_term_stack [in MetaRocq.SafeChecker.PCUICSafeConversion]
eqb_univ_instance [in MetaRocq.Common.uGraph]
eqb_univ_instance_gen [in MetaRocq.Common.uGraph]
eqb_global_decl [in MetaRocq.PCUIC.Syntax.PCUICReflect]
eqb_mutual_inductive_body [in MetaRocq.PCUIC.Syntax.PCUICReflect]
eqb_one_inductive_body [in MetaRocq.PCUIC.Syntax.PCUICReflect]
eqb_projection_body [in MetaRocq.PCUIC.Syntax.PCUICReflect]
eqb_constructor_body [in MetaRocq.PCUIC.Syntax.PCUICReflect]
eqb_constant_body [in MetaRocq.PCUIC.Syntax.PCUICReflect]
eqb_context_decl [in MetaRocq.PCUIC.Syntax.PCUICReflect]
eqb_predicate [in MetaRocq.PCUIC.Syntax.PCUICReflect]
eqb_term [in MetaRocq.PCUIC.Syntax.PCUICReflect]
eqb_predicate [in MetaRocq.Template.Ast]
eqb_list [in MetaRocq.Utils.ReflectEq]
eqb_prim_val [in MetaRocq.Erasure.EPrimitive]
eqb_prim_model [in MetaRocq.Erasure.EPrimitive]
eqb_array [in MetaRocq.Erasure.EPrimitive]
eqb_prim_val [in MetaRocq.PCUIC.utils.PCUICPrimitive]
eqb_prim_model [in MetaRocq.PCUIC.utils.PCUICPrimitive]
eqb_array [in MetaRocq.PCUIC.utils.PCUICPrimitive]
EqDec_ReflectEq [in MetaRocq.Utils.ReflectEq]
eqt [in MetaRocq.SafeChecker.PCUICSafeConversion]
Equal_graph [in MetaRocq.Common.uGraph]
equiv_env_inter [in MetaRocq.Erasure.ErasureFunction]
equiv_decls_inter [in MetaRocq.Erasure.ErasureFunction]
eq_termp_napp [in MetaRocq.PCUIC.PCUICCumulativity]
eq_decl_upto_gen [in MetaRocq.PCUIC.PCUICEquality]
eq_binder_annot_refl [in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_napp_sind [in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_napp_rec [in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_napp_ind [in MetaRocq.PCUIC.PCUICEquality]
eq_term_upto_univ_napp_rect [in MetaRocq.PCUIC.PCUICEquality]
eq_mfixpoint [in MetaRocq.PCUIC.PCUICEquality]
eq_branches [in MetaRocq.PCUIC.PCUICEquality]
eq_branch [in MetaRocq.PCUIC.PCUICEquality]
eq_predicate [in MetaRocq.PCUIC.PCUICEquality]
eq_decl_upto_names_sind [in MetaRocq.PCUIC.PCUICEquality]
eq_decl_upto_names_rec [in MetaRocq.PCUIC.PCUICEquality]
eq_decl_upto_names_ind [in MetaRocq.PCUIC.PCUICEquality]
eq_decl_upto_names_rect [in MetaRocq.PCUIC.PCUICEquality]
eq_leq_sort' [in MetaRocq.Common.Universes]
eq_sort [in MetaRocq.Common.Universes]
eq_sort_ [in MetaRocq.Common.Universes]
eq_leq_universe' [in MetaRocq.Common.Universes]
eq_universe [in MetaRocq.Common.Universes]
eq_binder_annot_refl [in MetaRocq.Template.TermEquality]
eq_term_upto_univ_napp_sind [in MetaRocq.Template.TermEquality]
eq_term_upto_univ_napp_rec [in MetaRocq.Template.TermEquality]
eq_term_upto_univ_napp_ind [in MetaRocq.Template.TermEquality]
eq_term_upto_univ_napp_rect [in MetaRocq.Template.TermEquality]
eq_decl_upto_names_sind [in MetaRocq.Template.TermEquality]
eq_decl_upto_names_rec [in MetaRocq.Template.TermEquality]
eq_decl_upto_names_ind [in MetaRocq.Template.TermEquality]
eq_decl_upto_names_rect [in MetaRocq.Template.TermEquality]
eq_term_upto_univ_refl_wf [in MetaRocq.SafeChecker.PCUICEqualityDec]
eq_cast_kind [in MetaRocq.Common.Reflect]
eq_def [in MetaRocq.Common.Reflect]
eq_aname [in MetaRocq.Common.Reflect]
eq_relevance [in MetaRocq.Common.Reflect]
eq_name [in MetaRocq.Common.Reflect]
eq_levels [in MetaRocq.Common.Reflect]
eq_prop_level [in MetaRocq.Common.Reflect]
eq_sort_dec [in MetaRocq.Common.UniversesDec]
eq_sort__dec [in MetaRocq.Common.UniversesDec]
eq_universe_dec [in MetaRocq.Common.UniversesDec]
eq_binder_annot [in MetaRocq.Common.BasicAst]
eq_context [in MetaRocq.Template.Typing]
eq_decl [in MetaRocq.Template.Typing]
eq_opt_term [in MetaRocq.Template.Typing]
eq_term_nocast [in MetaRocq.Template.Typing]
eq_term [in MetaRocq.Template.Checker]
eq_case_info [in MetaRocq.Template.Checker]
eq_max [in MetaRocq.Utils.wGraph]
eq_projection [in MetaRocq.Common.Kernames]
eq_inductive_def [in MetaRocq.Common.Kernames]
eq_constant [in MetaRocq.Common.Kernames]
eq_term_prop [in MetaRocq.PCUIC.PCUICCumulProp]
eq_univ_prop [in MetaRocq.PCUIC.PCUICCumulProp]
eq_simpl_pred [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
eq_prod [in MetaRocq.Utils.ReflectEq]
eq_sig_true [in MetaRocq.Utils.ReflectEq]
eq_bool [in MetaRocq.Utils.ReflectEq]
eq_option [in MetaRocq.Utils.ReflectEq]
eq_dec_to_bool [in MetaRocq.Utils.ReflectEq]
eq0_universe [in MetaRocq.Common.Universes]
eq0_universe_dec [in MetaRocq.Common.UniversesDec]
erase [in MetaRocq.Erasure.ErasureFunction]
erases_deps_sind [in MetaRocq.Erasure.Extract]
erases_deps_ind [in MetaRocq.Erasure.Extract]
erases_global [in MetaRocq.Erasure.Extract]
erases_global_decls_sind [in MetaRocq.Erasure.Extract]
erases_global_decls_ind [in MetaRocq.Erasure.Extract]
erases_mutual_inductive_body [in MetaRocq.Erasure.Extract]
erases_one_inductive_body [in MetaRocq.Erasure.Extract]
erases_constant_body [in MetaRocq.Erasure.Extract]
erases_sind [in MetaRocq.Erasure.Extract]
erases_ind [in MetaRocq.Erasure.Extract]
erase_global_decls_recursive [in MetaRocq.Erasure.Typed.Erasure]
erase_global_decls_deps_recursive [in MetaRocq.Erasure.Typed.Erasure]
erase_global_decl [in MetaRocq.Erasure.Typed.Erasure]
erase_ind [in MetaRocq.Erasure.Typed.Erasure]
erase_ind_body [in MetaRocq.Erasure.Typed.Erasure]
erase_ind_ctor [in MetaRocq.Erasure.Typed.Erasure]
erase_ind_arity [in MetaRocq.Erasure.Typed.Erasure]
erase_constant_decl [in MetaRocq.Erasure.Typed.Erasure]
erase_arity [in MetaRocq.Erasure.Typed.Erasure]
erase_type_scheme [in MetaRocq.Erasure.Typed.Erasure]
erase_type_scheme_eta [in MetaRocq.Erasure.Typed.Erasure]
erase_type_scheme_viewc [in MetaRocq.Erasure.Typed.Erasure]
erase_type_scheme_view_sind [in MetaRocq.Erasure.Typed.Erasure]
erase_type_scheme_view_rec [in MetaRocq.Erasure.Typed.Erasure]
erase_type_scheme_view_ind [in MetaRocq.Erasure.Typed.Erasure]
erase_type_scheme_view_rect [in MetaRocq.Erasure.Typed.Erasure]
erase_type [in MetaRocq.Erasure.Typed.Erasure]
erase_type_aux [in MetaRocq.Erasure.Typed.Erasure]
erase_type_viewc [in MetaRocq.Erasure.Typed.Erasure]
erase_type_view_sind [in MetaRocq.Erasure.Typed.Erasure]
erase_type_view_rec [in MetaRocq.Erasure.Typed.Erasure]
erase_type_view_ind [in MetaRocq.Erasure.Typed.Erasure]
erase_type_view_rect [in MetaRocq.Erasure.Typed.Erasure]
erase_type_discr [in MetaRocq.Erasure.Typed.Erasure]
erase_rel [in MetaRocq.Erasure.Typed.Erasure]
erase_global [in MetaRocq.Erasure.ErasureFunction]
erase_global_deps [in MetaRocq.Erasure.ErasureFunction]
erase_constant_decl [in MetaRocq.Erasure.ErasureFunction]
erase_mutual_inductive_body [in MetaRocq.Erasure.ErasureFunction]
erase_one_inductive_body [in MetaRocq.Erasure.ErasureFunction]
erase_constant_body [in MetaRocq.Erasure.ErasureFunction]
erase_cofix [in MetaRocq.Erasure.ErasureFunction]
erase_fix [in MetaRocq.Erasure.ErasureFunction]
erase_brs [in MetaRocq.Erasure.ErasureFunction]
erase_terms [in MetaRocq.Erasure.ErasureFunction]
erase_constant_decl_impl [in MetaRocq.Erasure.Typed.TypeAnnotations]
erase_type_of [in MetaRocq.Erasure.Typed.TypeAnnotations]
erase_type_aux_impl [in MetaRocq.Erasure.Typed.TypeAnnotations]
erase_global_fast [in MetaRocq.Erasure.ErasureFunctionProperties]
erase_global_deps_fast [in MetaRocq.Erasure.ErasureFunctionProperties]
erase_correct_firstorder [in MetaRocq.Erasure.ErasureFunctionProperties]
erase_nin [in MetaRocq.ErasurePlugin.ErasureCorrectness]
erase_decl_equal [in MetaRocq.ErasurePlugin.ErasureCorrectness]
erase_preserves_inductives [in MetaRocq.ErasurePlugin.ErasureCorrectness]
erase_term [in MetaRocq.Erasure.Typed.ExtractionCorrectness]
erase_env [in MetaRocq.Erasure.Typed.ExtractionCorrectness]
erase_program_typed [in MetaRocq.ErasurePlugin.ETransform]
erase_transform [in MetaRocq.ErasurePlugin.ETransform]
erase_program [in MetaRocq.ErasurePlugin.ETransform]
erase_pcuic_program [in MetaRocq.ErasurePlugin.ETransform]
erase_and_print_template_program [in MetaRocq.ErasurePlugin.Erasure]
erase_transform_mapping [in MetaRocq.ErasurePlugin.Erasure]
erase_prim_val_sind [in MetaRocq.Erasure.Extract]
erase_prim_val_ind [in MetaRocq.Erasure.Extract]
erase_prim_model_sind [in MetaRocq.Erasure.Extract]
erase_prim_model_rec [in MetaRocq.Erasure.Extract]
erase_prim_model_ind [in MetaRocq.Erasure.Extract]
erase_prim_model_rect [in MetaRocq.Erasure.Extract]
erase_context [in MetaRocq.Erasure.Extract]
erasure_pipeline_mapping [in MetaRocq.ErasurePlugin.Erasure]
erasure_pipeline [in MetaRocq.ErasurePlugin.Erasure]
eta_byte [in MetaRocq.Utils.ByteCompareSpec]
eta_expand_program [in MetaRocq.Template.EtaExpand]
eta_expand_global_env [in MetaRocq.Template.EtaExpand]
eta_global_declarations [in MetaRocq.Template.EtaExpand]
eta_global_declaration [in MetaRocq.Template.EtaExpand]
eta_minductive_decl [in MetaRocq.Template.EtaExpand]
eta_inductive_decl [in MetaRocq.Template.EtaExpand]
eta_constructor_decl [in MetaRocq.Template.EtaExpand]
eta_context [in MetaRocq.Template.EtaExpand]
eta_global_decl [in MetaRocq.Template.EtaExpand]
eta_expand [in MetaRocq.Template.EtaExpand]
eta_fixpoint [in MetaRocq.Template.EtaExpand]
eta_constructor [in MetaRocq.Template.EtaExpand]
eta_single [in MetaRocq.Template.EtaExpand]
eta_expand_def [in MetaRocq.Erasure.Typed.CertifyingEta]
eta_global_env_template [in MetaRocq.Erasure.Typed.CertifyingEta]
eta_global_env [in MetaRocq.Erasure.Typed.CertifyingEta]
eta_expand [in MetaRocq.Erasure.Typed.CertifyingEta]
eta_const [in MetaRocq.Erasure.Typed.CertifyingEta]
eta_ctor [in MetaRocq.Erasure.Typed.CertifyingEta]
eta_single [in MetaRocq.Erasure.Typed.CertifyingEta]
eta_expand [in MetaRocq.Template.TemplateCheckWf]
eta_expand_mapping [in MetaRocq.ErasurePlugin.Erasure]
eta_expand [in MetaRocq.ErasurePlugin.Erasure]
ETransformPresFO.compose_compile_fo_value [in MetaRocq.ErasurePlugin.ErasureCorrectness]
eval_template_program_env [in MetaRocq.Template.TemplateProgram]
eval_template_program [in MetaRocq.Template.TemplateProgram]
eval_inlined_program [in MetaRocq.Erasure.EInlining]
eval_evals_ind [in MetaRocq.Template.WcbvEval]
eval_sind [in MetaRocq.Template.WcbvEval]
eval_rec [in MetaRocq.Template.WcbvEval]
eval_ind [in MetaRocq.Template.WcbvEval]
eval_rect [in MetaRocq.Template.WcbvEval]
eval_prim_length [in MetaRocq.Erasure.Typed.WcbvEvalAux]
eval_eprogram_env [in MetaRocq.Erasure.EProgram]
eval_eprogram [in MetaRocq.Erasure.EProgram]
eval_eprogram_env_mapping [in MetaRocq.ErasurePlugin.ETransform]
eval_eprogram_mapping [in MetaRocq.ErasurePlugin.ETransform]
eval_typed_eprogram_masks [in MetaRocq.ErasurePlugin.ETransform]
eval_typed_eprogram [in MetaRocq.ErasurePlugin.ETransform]
eval_nondep [in MetaRocq.Erasure.EWcbvEval]
eval_ind [in MetaRocq.Erasure.EWcbvEval]
eval_rec [in MetaRocq.Erasure.EWcbvEval]
eval_depth [in MetaRocq.Erasure.EWcbvEval]
eval_primitive_depth [in MetaRocq.Erasure.EWcbvEval]
eval_typed_eprogram_masks_mapping [in MetaRocq.ErasurePlugin.Erasure]
eval_typed_eprogram_mapping [in MetaRocq.ErasurePlugin.Erasure]
eval_template_program_env_mapping [in MetaRocq.ErasurePlugin.Erasure]
eval_template_program_mapping [in MetaRocq.ErasurePlugin.Erasure]
eval_pcuic_program_mapping [in MetaRocq.ErasurePlugin.Erasure]
eval_ind [in MetaRocq.Erasure.EWcbvEvalNamed]
eval_ind [in MetaRocq.PCUIC.PCUICWcbvEval]
eval_rect [in MetaRocq.PCUIC.PCUICWcbvEval]
eval_pcuic_program [in MetaRocq.TemplatePCUIC.PCUICTransform]
even [in MetaRocq.Examples.demo]
expanded_eprogram_env_cstrs [in MetaRocq.Erasure.EEtaExpanded]
expanded_eprogram_cstrs [in MetaRocq.Erasure.EEtaExpanded]
expanded_global_env [in MetaRocq.Erasure.EEtaExpanded]
expanded_global_declarations_sind [in MetaRocq.Erasure.EEtaExpanded]
expanded_global_declarations_ind [in MetaRocq.Erasure.EEtaExpanded]
expanded_decl [in MetaRocq.Erasure.EEtaExpanded]
expanded_constant_decl [in MetaRocq.Erasure.EEtaExpanded]
expanded_program [in MetaRocq.Template.EtaExpand]
expanded_global_env [in MetaRocq.Template.EtaExpand]
expanded_global_declarations_sind [in MetaRocq.Template.EtaExpand]
expanded_global_declarations_ind [in MetaRocq.Template.EtaExpand]
expanded_decl [in MetaRocq.Template.EtaExpand]
expanded_context [in MetaRocq.Template.EtaExpand]
expanded_pcuic_program [in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_global_env [in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_global_declarations_sind [in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_global_declarations_ind [in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_decl [in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_context [in MetaRocq.PCUIC.PCUICEtaExpand]
expanded_head_viewc [in MetaRocq.Erasure.EEtaExpandedFix]
expanded_head_view_sind [in MetaRocq.Erasure.EEtaExpandedFix]
expanded_head_view_rec [in MetaRocq.Erasure.EEtaExpandedFix]
expanded_head_view_ind [in MetaRocq.Erasure.EEtaExpandedFix]
expanded_head_view_rect [in MetaRocq.Erasure.EEtaExpandedFix]
expanded_eprogram_env [in MetaRocq.Erasure.EEtaExpandedFix]
expanded_eprogram [in MetaRocq.Erasure.EEtaExpandedFix]
expanded_global_env [in MetaRocq.Erasure.EEtaExpandedFix]
expanded_global_declarations_sind [in MetaRocq.Erasure.EEtaExpandedFix]
expanded_global_declarations_ind [in MetaRocq.Erasure.EEtaExpandedFix]
expanded_decl [in MetaRocq.Erasure.EEtaExpandedFix]
expanded_constant_decl [in MetaRocq.Erasure.EEtaExpandedFix]
expand_lets_program [in MetaRocq.PCUIC.PCUICExpandLets]
expand_lets_k_ctx_decl [in MetaRocq.PCUIC.PCUICSigmaCalculus]
expand_lets_k_ctx_vass [in MetaRocq.PCUIC.PCUICSigmaCalculus]
extendP [in MetaRocq.PCUIC.PCUICParallelReduction]
extends [in MetaRocq.Erasure.EGlobalEnv]
extends_global_env [in MetaRocq.Erasure.ErasureFunction]
extends_inlined_eprogram [in MetaRocq.Erasure.EInlining]
extends_eprogram_env [in MetaRocq.Erasure.EProgram]
extends_eprogram [in MetaRocq.Erasure.EProgram]
extends_pcuic_program [in MetaRocq.ErasurePlugin.ETransform]
extends_global_env [in MetaRocq.ErasurePlugin.ETransform]
extends_prefix [in MetaRocq.Erasure.EGlobalEnv]
extends_strictly_on_decls_wf_local [in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
extends_decls_wf_local [in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
extends_wf_local [in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
extend_over [in MetaRocq.PCUIC.PCUICParallelReduction]
extraction_wcbv_flags [in MetaRocq.Erasure.EWcbvEvalNamed]
extraction_env_flags [in MetaRocq.Erasure.EWcbvEvalNamed]
extraction_term_flags [in MetaRocq.Erasure.EWcbvEvalNamed]
ExtractTransform [in MetaRocq.Erasure.Typed.Transform]
ExtractTransformCorrect [in MetaRocq.Erasure.Typed.Transform]
extract_form [in MetaRocq.Examples.tauto]
extract_template_env_within_coq [in MetaRocq.Erasure.Typed.Extraction]
extract_within_coq [in MetaRocq.Erasure.Typed.Extraction]
extract_template_env_certifying_passes [in MetaRocq.Erasure.Typed.Extraction]
extract_template_env [in MetaRocq.Erasure.Typed.Extraction]
extract_template_env_general [in MetaRocq.Erasure.Typed.Extraction]
extract_pcuic_env [in MetaRocq.Erasure.Typed.Extraction]
extract_def_name [in MetaRocq.Erasure.Typed.Utils]
extract_def_name [in MetaRocq.Erasure.Typed.CertifyingEta]
extract_def_name [in MetaRocq.Erasure.Typed.CertifyingBeta]
extract_def_name [in MetaRocq.Erasure.Typed.CertifyingInlining]
| 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) |