| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (75519 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (245 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (61331 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (144 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (89 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (236 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6913 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1141 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (34 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (269 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (443 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (296 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (604 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (248 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3386 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (140 entries) |
E (definition)
eckmann_hilton [in MetaCoq.Translations.MiniHoTT]eckmann_hilton [in MetaCoq.Translations.MiniHoTT_paths]
EdgeSet_triple [in MetaCoq.Template.common.uGraph]
EdgeSet_pair [in MetaCoq.Template.common.uGraph]
edge_of_constraint [in MetaCoq.Template.common.uGraph]
edge_of_level [in MetaCoq.Template.common.uGraph]
emax [in MetaCoq.Template.BasicAst]
emptyTC [in MetaCoq.Translations.translation_utils]
empty_ext [in MetaCoq.PCUIC.utils.PCUICAstUtils]
empty_trans_env [in MetaCoq.PCUIC.TemplateToPCUIC]
EnvCheck_wf_env_ext [in MetaCoq.SafeChecker.SafeTemplateChecker]
EnvCheck_X_env_ext_type [in MetaCoq.SafeChecker.PCUICSafeChecker]
Environment.add_global_decl [in MetaCoq.Template.Environment]
Environment.All2_fold_over [in MetaCoq.Template.Environment]
Environment.app_context [in MetaCoq.Template.Environment]
Environment.arities_context [in MetaCoq.Template.Environment]
Environment.context [in MetaCoq.Template.Environment]
Environment.context_assumptions [in MetaCoq.Template.Environment]
Environment.empty_ext [in MetaCoq.Template.Environment]
Environment.empty_global_env [in MetaCoq.Template.Environment]
Environment.expand_lets_ctx [in MetaCoq.Template.Environment]
Environment.expand_lets_k_ctx [in MetaCoq.Template.Environment]
Environment.expand_lets [in MetaCoq.Template.Environment]
Environment.expand_lets_k [in MetaCoq.Template.Environment]
Environment.extended_subst [in MetaCoq.Template.Environment]
Environment.extends [in MetaCoq.Template.Environment]
Environment.extends_decls [in MetaCoq.Template.Environment]
Environment.fix_context [in MetaCoq.Template.Environment]
Environment.fst_ctx [in MetaCoq.Template.Environment]
Environment.global_env_ext [in MetaCoq.Template.Environment]
Environment.global_declarations [in MetaCoq.Template.Environment]
Environment.is_assumption_context [in MetaCoq.Template.Environment]
Environment.it_mkProd_or_LetIn [in MetaCoq.Template.Environment]
Environment.it_mkLambda_or_LetIn [in MetaCoq.Template.Environment]
Environment.lift_context [in MetaCoq.Template.Environment]
Environment.lift_decl [in MetaCoq.Template.Environment]
Environment.lookup_env [in MetaCoq.Template.Environment]
Environment.lookup_global [in MetaCoq.Template.Environment]
Environment.map_mutual_inductive_body [in MetaCoq.Template.Environment]
Environment.map_constant_body [in MetaCoq.Template.Environment]
Environment.map_one_inductive_body [in MetaCoq.Template.Environment]
Environment.map_projection_body [in MetaCoq.Template.Environment]
Environment.map_constructor_body [in MetaCoq.Template.Environment]
Environment.mkLambda_or_LetIn [in MetaCoq.Template.Environment]
Environment.mkProd_or_LetIn [in MetaCoq.Template.Environment]
Environment.program [in MetaCoq.Template.Environment]
Environment.projs [in MetaCoq.Template.Environment]
Environment.reln [in MetaCoq.Template.Environment]
Environment.reln_alt [in MetaCoq.Template.Environment]
Environment.set_binder_name [in MetaCoq.Template.Environment]
Environment.smash_context [in MetaCoq.Template.Environment]
Environment.subst_telescope [in MetaCoq.Template.Environment]
Environment.subst_decl [in MetaCoq.Template.Environment]
Environment.subst_context [in MetaCoq.Template.Environment]
Environment.to_extended_list [in MetaCoq.Template.Environment]
Environment.to_extended_list_k [in MetaCoq.Template.Environment]
Environment.typ_or_sort [in MetaCoq.Template.Environment]
Environment.vass [in MetaCoq.Template.Environment]
Environment.vdef [in MetaCoq.Template.Environment]
EnvMap.add [in MetaCoq.Template.EnvMap]
EnvMap.empty [in MetaCoq.Template.EnvMap]
EnvMap.equal [in MetaCoq.Template.EnvMap]
EnvMap.fresh_global [in MetaCoq.Template.EnvMap]
EnvMap.lookup [in MetaCoq.Template.EnvMap]
EnvMap.lookup_global [in MetaCoq.Template.EnvMap]
EnvMap.of_global_env [in MetaCoq.Template.EnvMap]
EnvMap.remove [in MetaCoq.Template.EnvMap]
EnvMap.repr [in MetaCoq.Template.EnvMap]
EnvMap.t [in MetaCoq.Template.EnvMap]
EnvTyping.All_local_rel_sorting_size [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_env_sorting_size [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_rel_size [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_env_size [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_env_size_gen [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_env_over_sorting [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_env_over [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_rel_def [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_rel_abs [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_rel_nil [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_rel [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.infer_sort [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.lift_sorting_size [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.lift_typing_size [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.lift_judgment_size [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.lift_typing2 [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.lift_sorting [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.lift_typing [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.lift_wf_term [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.lift_judgment [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.on_def_body [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.on_def_type [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.on_local_decl [in MetaCoq.Template.EnvironmentTyping]
env_prop_bd [in MetaCoq.PCUIC.Bidirectional.BDTyping]
env_prop [in MetaCoq.Template.Typing]
env_flags_blocks [in MetaCoq.Erasure.EConstructorsAsBlocks]
env_flags [in MetaCoq.Erasure.EConstructorsAsBlocks]
env_prop [in MetaCoq.PCUIC.PCUICTyping]
eprogram [in MetaCoq.Erasure.EProgram]
eprogram_env [in MetaCoq.Erasure.EProgram]
eqb [in MetaCoq.Template.utils.ByteCompare]
eqb_binder_annot [in MetaCoq.Template.BasicAst]
eqb_compare [in MetaCoq.Template.utils.ByteCompareSpec]
eqb_predicate [in MetaCoq.Template.Ast]
eqb_univ_instance [in MetaCoq.Template.common.uGraph]
eqb_list [in MetaCoq.Template.utils.ReflectEq]
eqb_predicate [in MetaCoq.PCUIC.PCUICAst]
eqb_predicate_gen [in MetaCoq.PCUIC.PCUICAst]
eqb_universe_instance [in MetaCoq.SafeChecker.PCUICSafeConversion]
eqb_universe_instance_gen [in MetaCoq.SafeChecker.PCUICSafeConversion]
eqb_term_stack [in MetaCoq.SafeChecker.PCUICSafeConversion]
eqb_Variance [in MetaCoq.Template.Reflect]
eqb_allowed_eliminations [in MetaCoq.Template.Reflect]
eqb_universes_decl [in MetaCoq.Template.Reflect]
eqb_ConstraintType [in MetaCoq.Template.Reflect]
eqb_recursivity_kind [in MetaCoq.Template.Reflect]
eqb_context_decl [in MetaCoq.Template.Reflect]
eqb_case_info [in MetaCoq.Template.Reflect]
eqb_global_decl [in MetaCoq.PCUIC.Syntax.PCUICReflect]
eqb_mutual_inductive_body [in MetaCoq.PCUIC.Syntax.PCUICReflect]
eqb_one_inductive_body [in MetaCoq.PCUIC.Syntax.PCUICReflect]
eqb_projection_body [in MetaCoq.PCUIC.Syntax.PCUICReflect]
eqb_constructor_body [in MetaCoq.PCUIC.Syntax.PCUICReflect]
eqb_constant_body [in MetaCoq.PCUIC.Syntax.PCUICReflect]
eqb_context_decl [in MetaCoq.PCUIC.Syntax.PCUICReflect]
eqb_predicate [in MetaCoq.PCUIC.Syntax.PCUICReflect]
eqb_term [in MetaCoq.PCUIC.Syntax.PCUICReflect]
eqb_global_decl [in MetaCoq.Erasure.EReflect]
eqb_mutual_inductive_body [in MetaCoq.Erasure.EReflect]
eqb_one_inductive_body [in MetaCoq.Erasure.EReflect]
eqb_projection_body [in MetaCoq.Erasure.EReflect]
eqb_constructor_body [in MetaCoq.Erasure.EReflect]
eqb_constant_body [in MetaCoq.Erasure.EReflect]
eqb_opt_term [in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_term [in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_termp [in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_termp_napp [in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_ctx [in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_ctx_gen_proper [in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_ctx_gen [in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_term_upto_univ_proper [in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_univ_reflect [in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_termp_napp_gen [in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_term_upto_univ_napp [in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_binder_annots [in MetaCoq.SafeChecker.PCUICEqualityDec]
EqDec_ReflectEq [in MetaCoq.Template.utils.ReflectEq]
eqt [in MetaCoq.SafeChecker.PCUICSafeConversion]
Equal_graph [in MetaCoq.Template.common.uGraph]
equiv [in MetaCoq.Translations.times_bool_fun2]
equiv [in MetaCoq.Translations.param_generous_packed]
equiv_sigma_assoc [in MetaCoq.Translations.MiniHoTT]
equiv_contr_sigma [in MetaCoq.Translations.MiniHoTT]
equiv_sigma_contr [in MetaCoq.Translations.MiniHoTT]
equiv_functor_sigma_id [in MetaCoq.Translations.MiniHoTT]
equiv_functor_sigma' [in MetaCoq.Translations.MiniHoTT]
equiv_functor_sigma [in MetaCoq.Translations.MiniHoTT]
equiv_path_sigma_contra [in MetaCoq.Translations.MiniHoTT]
equiv_path_sigma [in MetaCoq.Translations.MiniHoTT]
equiv_flip [in MetaCoq.Translations.MiniHoTT]
equiv_contr_forall [in MetaCoq.Translations.MiniHoTT]
equiv_functor_forall_covariant_compose [in MetaCoq.Translations.MiniHoTT]
equiv_functor_forall_covariant [in MetaCoq.Translations.MiniHoTT]
equiv_functor_forall_pf [in MetaCoq.Translations.MiniHoTT]
equiv_functor_forall_pb [in MetaCoq.Translations.MiniHoTT]
equiv_functor_forall_id [in MetaCoq.Translations.MiniHoTT]
equiv_functor_forall' [in MetaCoq.Translations.MiniHoTT]
equiv_functor_forall [in MetaCoq.Translations.MiniHoTT]
equiv_path_forall [in MetaCoq.Translations.MiniHoTT]
equiv_apD10 [in MetaCoq.Translations.MiniHoTT]
equiv_paths_ind [in MetaCoq.Translations.MiniHoTT]
equiv_moveL_equiv_V [in MetaCoq.Translations.MiniHoTT]
equiv_moveL_equiv_M [in MetaCoq.Translations.MiniHoTT]
equiv_moveR_equiv_V [in MetaCoq.Translations.MiniHoTT]
equiv_moveR_equiv_M [in MetaCoq.Translations.MiniHoTT]
equiv_moveL_transport_p [in MetaCoq.Translations.MiniHoTT]
equiv_moveL_transport_V [in MetaCoq.Translations.MiniHoTT]
equiv_moveR_transport_V [in MetaCoq.Translations.MiniHoTT]
equiv_moveR_transport_p [in MetaCoq.Translations.MiniHoTT]
equiv_moveL_pV [in MetaCoq.Translations.MiniHoTT]
equiv_moveL_Vp [in MetaCoq.Translations.MiniHoTT]
equiv_moveL_pM [in MetaCoq.Translations.MiniHoTT]
equiv_moveL_Mp [in MetaCoq.Translations.MiniHoTT]
equiv_moveR_pV [in MetaCoq.Translations.MiniHoTT]
equiv_moveR_Vp [in MetaCoq.Translations.MiniHoTT]
equiv_moveR_pM [in MetaCoq.Translations.MiniHoTT]
equiv_moveR_Mp [in MetaCoq.Translations.MiniHoTT]
equiv_cancelR [in MetaCoq.Translations.MiniHoTT]
equiv_whiskerR [in MetaCoq.Translations.MiniHoTT]
equiv_cancelL [in MetaCoq.Translations.MiniHoTT]
equiv_whiskerL [in MetaCoq.Translations.MiniHoTT]
equiv_concat_lr [in MetaCoq.Translations.MiniHoTT]
equiv_concat_r [in MetaCoq.Translations.MiniHoTT]
equiv_concat_l [in MetaCoq.Translations.MiniHoTT]
equiv_path_inverse [in MetaCoq.Translations.MiniHoTT]
equiv_inj [in MetaCoq.Translations.MiniHoTT]
equiv_ap' [in MetaCoq.Translations.MiniHoTT]
equiv_ap [in MetaCoq.Translations.MiniHoTT]
equiv_composeR' [in MetaCoq.Translations.MiniHoTT]
equiv_ind_comp [in MetaCoq.Translations.MiniHoTT]
equiv_ind [in MetaCoq.Translations.MiniHoTT]
equiv_postcompose' [in MetaCoq.Translations.MiniHoTT]
equiv_postcompose [in MetaCoq.Translations.MiniHoTT]
equiv_precompose' [in MetaCoq.Translations.MiniHoTT]
equiv_precompose [in MetaCoq.Translations.MiniHoTT]
equiv_involution [in MetaCoq.Translations.MiniHoTT]
equiv_adjointify [in MetaCoq.Translations.MiniHoTT]
equiv_transport [in MetaCoq.Translations.MiniHoTT]
equiv_homotopic [in MetaCoq.Translations.MiniHoTT]
equiv_compose' [in MetaCoq.Translations.MiniHoTT]
equiv_compose [in MetaCoq.Translations.MiniHoTT]
equiv_idmap [in MetaCoq.Translations.MiniHoTT]
equiv_sigma_assoc [in MetaCoq.Translations.MiniHoTT_paths]
equiv_contr_sigma [in MetaCoq.Translations.MiniHoTT_paths]
equiv_sigma_contr [in MetaCoq.Translations.MiniHoTT_paths]
equiv_functor_sigma_id [in MetaCoq.Translations.MiniHoTT_paths]
equiv_functor_sigma' [in MetaCoq.Translations.MiniHoTT_paths]
equiv_functor_sigma [in MetaCoq.Translations.MiniHoTT_paths]
equiv_path_sigma_contra [in MetaCoq.Translations.MiniHoTT_paths]
equiv_path_sigma [in MetaCoq.Translations.MiniHoTT_paths]
equiv_flip [in MetaCoq.Translations.MiniHoTT_paths]
equiv_contr_forall [in MetaCoq.Translations.MiniHoTT_paths]
equiv_functor_forall_covariant_compose [in MetaCoq.Translations.MiniHoTT_paths]
equiv_functor_forall_covariant [in MetaCoq.Translations.MiniHoTT_paths]
equiv_functor_forall_pf [in MetaCoq.Translations.MiniHoTT_paths]
equiv_functor_forall_pb [in MetaCoq.Translations.MiniHoTT_paths]
equiv_functor_forall_id [in MetaCoq.Translations.MiniHoTT_paths]
equiv_functor_forall' [in MetaCoq.Translations.MiniHoTT_paths]
equiv_functor_forall [in MetaCoq.Translations.MiniHoTT_paths]
equiv_path_forall [in MetaCoq.Translations.MiniHoTT_paths]
equiv_apD10 [in MetaCoq.Translations.MiniHoTT_paths]
equiv_paths_ind [in MetaCoq.Translations.MiniHoTT_paths]
equiv_moveL_equiv_V [in MetaCoq.Translations.MiniHoTT_paths]
equiv_moveL_equiv_M [in MetaCoq.Translations.MiniHoTT_paths]
equiv_moveR_equiv_V [in MetaCoq.Translations.MiniHoTT_paths]
equiv_moveR_equiv_M [in MetaCoq.Translations.MiniHoTT_paths]
equiv_moveL_transport_p [in MetaCoq.Translations.MiniHoTT_paths]
equiv_moveL_transport_V [in MetaCoq.Translations.MiniHoTT_paths]
equiv_moveR_transport_V [in MetaCoq.Translations.MiniHoTT_paths]
equiv_moveR_transport_p [in MetaCoq.Translations.MiniHoTT_paths]
equiv_moveL_pV [in MetaCoq.Translations.MiniHoTT_paths]
equiv_moveL_Vp [in MetaCoq.Translations.MiniHoTT_paths]
equiv_moveL_pM [in MetaCoq.Translations.MiniHoTT_paths]
equiv_moveL_Mp [in MetaCoq.Translations.MiniHoTT_paths]
equiv_moveR_pV [in MetaCoq.Translations.MiniHoTT_paths]
equiv_moveR_Vp [in MetaCoq.Translations.MiniHoTT_paths]
equiv_moveR_pM [in MetaCoq.Translations.MiniHoTT_paths]
equiv_moveR_Mp [in MetaCoq.Translations.MiniHoTT_paths]
equiv_cancelR [in MetaCoq.Translations.MiniHoTT_paths]
equiv_whiskerR [in MetaCoq.Translations.MiniHoTT_paths]
equiv_cancelL [in MetaCoq.Translations.MiniHoTT_paths]
equiv_whiskerL [in MetaCoq.Translations.MiniHoTT_paths]
equiv_concat_lr [in MetaCoq.Translations.MiniHoTT_paths]
equiv_concat_r [in MetaCoq.Translations.MiniHoTT_paths]
equiv_concat_l [in MetaCoq.Translations.MiniHoTT_paths]
equiv_path_inverse [in MetaCoq.Translations.MiniHoTT_paths]
equiv_inj [in MetaCoq.Translations.MiniHoTT_paths]
equiv_ap' [in MetaCoq.Translations.MiniHoTT_paths]
equiv_ap [in MetaCoq.Translations.MiniHoTT_paths]
equiv_composeR' [in MetaCoq.Translations.MiniHoTT_paths]
equiv_ind_comp [in MetaCoq.Translations.MiniHoTT_paths]
equiv_ind [in MetaCoq.Translations.MiniHoTT_paths]
equiv_postcompose' [in MetaCoq.Translations.MiniHoTT_paths]
equiv_postcompose [in MetaCoq.Translations.MiniHoTT_paths]
equiv_precompose' [in MetaCoq.Translations.MiniHoTT_paths]
equiv_precompose [in MetaCoq.Translations.MiniHoTT_paths]
equiv_involution [in MetaCoq.Translations.MiniHoTT_paths]
equiv_adjointify [in MetaCoq.Translations.MiniHoTT_paths]
equiv_transport [in MetaCoq.Translations.MiniHoTT_paths]
equiv_homotopic [in MetaCoq.Translations.MiniHoTT_paths]
equiv_compose' [in MetaCoq.Translations.MiniHoTT_paths]
equiv_compose [in MetaCoq.Translations.MiniHoTT_paths]
equiv_idmap [in MetaCoq.Translations.MiniHoTT_paths]
equiv_contrfib [in MetaCoq.Translations.times_bool_fun2]
eq_universe_leq_universe' [in MetaCoq.Template.Universes]
eq_universe [in MetaCoq.Template.Universes]
eq_universe_ [in MetaCoq.Template.Universes]
eq_levelalg [in MetaCoq.Template.Universes]
eq_binder_annot [in MetaCoq.Template.BasicAst]
eq_termp_napp [in MetaCoq.PCUIC.PCUICCumulativity]
eq_eqᵗ [in MetaCoq.Translations.times_bool_fun]
eq_context [in MetaCoq.Template.Typing]
eq_decl [in MetaCoq.Template.Typing]
eq_opt_term [in MetaCoq.Template.Typing]
eq_term_nocast [in MetaCoq.Template.Typing]
eq_binder_annot_refl [in MetaCoq.Template.TermEquality]
eq_simpl_pred [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
eq_term_prop [in MetaCoq.PCUIC.PCUICCumulProp]
eq_univ_prop [in MetaCoq.PCUIC.PCUICCumulProp]
eq_decl_upto_gen [in MetaCoq.PCUIC.PCUICEquality]
eq_binder_annot_refl [in MetaCoq.PCUIC.PCUICEquality]
eq_predicate [in MetaCoq.PCUIC.PCUICEquality]
eq_projection [in MetaCoq.Template.Kernames]
eq_inductive_def [in MetaCoq.Template.Kernames]
eq_constant [in MetaCoq.Template.Kernames]
eq_prod [in MetaCoq.Template.utils.ReflectEq]
eq_sig_true [in MetaCoq.Template.utils.ReflectEq]
eq_bool [in MetaCoq.Template.utils.ReflectEq]
eq_option [in MetaCoq.Template.utils.ReflectEq]
eq_dec_to_bool [in MetaCoq.Template.utils.ReflectEq]
eq_max [in MetaCoq.Template.utils.wGraph]
eq_term [in MetaCoq.Template.Checker]
eq_case_info [in MetaCoq.Template.Checker]
eq_cast_kind [in MetaCoq.Template.Reflect]
eq_def [in MetaCoq.Template.Reflect]
eq_aname [in MetaCoq.Template.Reflect]
eq_relevance [in MetaCoq.Template.Reflect]
eq_name [in MetaCoq.Template.Reflect]
eq_levels [in MetaCoq.Template.Reflect]
eq_prop_level [in MetaCoq.Template.Reflect]
eq_term_upto_univ_refl_wf [in MetaCoq.SafeChecker.PCUICEqualityDec]
eq0_levelalg [in MetaCoq.Template.Universes]
eqᵗ_eq [in MetaCoq.Translations.times_bool_fun]
erase [in MetaCoq.Erasure.ErasureFunction]
erases_global [in MetaCoq.Erasure.Extract]
erases_mutual_inductive_body [in MetaCoq.Erasure.Extract]
erases_one_inductive_body [in MetaCoq.Erasure.Extract]
erases_constant_body [in MetaCoq.Erasure.Extract]
erase_context [in MetaCoq.Erasure.Extract]
erase_global_fast [in MetaCoq.Erasure.ErasureFunction]
erase_global_decls_fast [in MetaCoq.Erasure.ErasureFunction]
erase_global_decls [in MetaCoq.Erasure.ErasureFunction]
erase_mutual_inductive_body [in MetaCoq.Erasure.ErasureFunction]
erase_one_inductive_body [in MetaCoq.Erasure.ErasureFunction]
erase_constant_body [in MetaCoq.Erasure.ErasureFunction]
erase_cofix [in MetaCoq.Erasure.ErasureFunction]
erase_fix [in MetaCoq.Erasure.ErasureFunction]
erase_brs [in MetaCoq.Erasure.ErasureFunction]
erase_terms [in MetaCoq.Erasure.ErasureFunction]
erase_prim [in MetaCoq.Erasure.ErasureFunction]
erase_transform [in MetaCoq.Erasure.ETransform]
erase_program [in MetaCoq.Erasure.ETransform]
erase_pcuic_program [in MetaCoq.Erasure.ETransform]
erase_fast_and_print_template_program [in MetaCoq.Erasure.Erasure]
erase_and_print_template_program [in MetaCoq.Erasure.Erasure]
erasure_pipeline_fast [in MetaCoq.Erasure.Erasure]
erasure_pipeline [in MetaCoq.Erasure.Erasure]
eta_expand_program [in MetaCoq.Template.EtaExpand]
eta_expand_global_env [in MetaCoq.Template.EtaExpand]
eta_global_declarations [in MetaCoq.Template.EtaExpand]
eta_global_declaration [in MetaCoq.Template.EtaExpand]
eta_minductive_decl [in MetaCoq.Template.EtaExpand]
eta_inductive_decl [in MetaCoq.Template.EtaExpand]
eta_constructor_decl [in MetaCoq.Template.EtaExpand]
eta_context [in MetaCoq.Template.EtaExpand]
eta_global_decl [in MetaCoq.Template.EtaExpand]
eta_expand [in MetaCoq.Template.EtaExpand]
eta_fixpoint [in MetaCoq.Template.EtaExpand]
eta_constructor [in MetaCoq.Template.EtaExpand]
eta_single [in MetaCoq.Template.EtaExpand]
eta_expand [in MetaCoq.Template.TemplateCheckWf]
eta_path_sigma [in MetaCoq.Translations.MiniHoTT]
eta_path_sigma_uncurried [in MetaCoq.Translations.MiniHoTT]
eta_sigma [in MetaCoq.Translations.MiniHoTT]
eta_path_forall [in MetaCoq.Translations.MiniHoTT]
eta_path_sigma [in MetaCoq.Translations.MiniHoTT_paths]
eta_path_sigma_uncurried [in MetaCoq.Translations.MiniHoTT_paths]
eta_sigma [in MetaCoq.Translations.MiniHoTT_paths]
eta_path_forall [in MetaCoq.Translations.MiniHoTT_paths]
eta2_sigma [in MetaCoq.Translations.MiniHoTT]
eta2_sigma [in MetaCoq.Translations.MiniHoTT_paths]
eta3_sigma [in MetaCoq.Translations.MiniHoTT]
eta3_sigma [in MetaCoq.Translations.MiniHoTT_paths]
eval_pcuic_program [in MetaCoq.PCUIC.PCUICTransform]
eval_template_program [in MetaCoq.Template.TemplateProgram]
eval_eprogram_env [in MetaCoq.Erasure.EProgram]
eval_eprogram [in MetaCoq.Erasure.EProgram]
eval_evals_ind [in MetaCoq.Template.WcbvEval]
eval_depth [in MetaCoq.Erasure.EWcbvEval]
eval_nondep [in MetaCoq.Erasure.EWcbvEval]
even [in MetaCoq.Examples.demo]
expanded_program [in MetaCoq.Template.EtaExpand]
expanded_global_env [in MetaCoq.Template.EtaExpand]
expanded_decl [in MetaCoq.Template.EtaExpand]
expanded_context [in MetaCoq.Template.EtaExpand]
expanded_head_viewc [in MetaCoq.Erasure.EEtaExpandedFix]
expanded_eprogram_env [in MetaCoq.Erasure.EEtaExpandedFix]
expanded_eprogram [in MetaCoq.Erasure.EEtaExpandedFix]
expanded_global_env [in MetaCoq.Erasure.EEtaExpandedFix]
expanded_decl [in MetaCoq.Erasure.EEtaExpandedFix]
expanded_constant_decl [in MetaCoq.Erasure.EEtaExpandedFix]
expanded_pcuic_program [in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_global_env [in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_decl [in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_context [in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_eprogram_env_cstrs [in MetaCoq.Erasure.EEtaExpanded]
expanded_eprogram_cstrs [in MetaCoq.Erasure.EEtaExpanded]
expanded_global_env [in MetaCoq.Erasure.EEtaExpanded]
expanded_decl [in MetaCoq.Erasure.EEtaExpanded]
expanded_constant_decl [in MetaCoq.Erasure.EEtaExpanded]
expand_lets_program [in MetaCoq.PCUIC.PCUICExpandLets]
expand_lets_k_ctx_decl [in MetaCoq.PCUIC.PCUICSigmaCalculus]
expand_lets_k_ctx_vass [in MetaCoq.PCUIC.PCUICSigmaCalculus]
extendP [in MetaCoq.PCUIC.PCUICParallelReduction]
extends [in MetaCoq.Erasure.EGlobalEnv]
extend_over [in MetaCoq.PCUIC.PCUICParallelReduction]
extract_form [in MetaCoq.Examples.tauto]
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (75519 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (245 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (61331 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (144 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (89 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (236 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6913 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1141 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (34 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (269 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (443 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (296 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (604 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (248 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3386 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (140 entries) |