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)

I (definition)

idecl_binder [in MetaCoq.PCUIC.Syntax.PCUICCases]
ident [in MetaCoq.Template.Kernames]
idequiv [in MetaCoq.Translations.times_bool_fun2]
idpath [in MetaCoq.Translations.MiniHoTT]
ids [in MetaCoq.PCUIC.PCUICSigmaCalculus]
idsn [in MetaCoq.PCUIC.PCUICSigmaCalculus]
id_nat [in MetaCoq.Examples.demo]
id2equiv [in MetaCoq.Translations.times_bool_fun2]
iffT_l [in MetaCoq.Template.utils.MCRelations]
Implement [in MetaCoq.Translations.translation_utils]
ImplementExisting [in MetaCoq.Translations.translation_utils]
includes_deps [in MetaCoq.Erasure.ErasureFunction]
inds [in MetaCoq.Template.Ast]
inds [in MetaCoq.PCUIC.PCUICAst]
inductive_arity [in MetaCoq.Erasure.Extract]
inductive_isprop_and_pars [in MetaCoq.Erasure.EGlobalEnv]
ind_predicate_context [in MetaCoq.Template.Ast]
ind_predicate_context [in MetaCoq.PCUIC.Syntax.PCUICCases]
ind_subst [in MetaCoq.PCUIC.Syntax.PCUICCases]
ind_binder [in MetaCoq.PCUIC.PCUICCasesContexts]
infer [in MetaCoq.SafeChecker.PCUICSafeRetyping]
infer [in MetaCoq.Template.Checker]
infer [in MetaCoq.SafeChecker.PCUICTypeChecker]
infering_indu_size_pos [in MetaCoq.PCUIC.Bidirectional.BDTyping]
infering_prod_size_pos [in MetaCoq.PCUIC.Bidirectional.BDTyping]
infering_sort_size_pos [in MetaCoq.PCUIC.Bidirectional.BDTyping]
infering_size_pos [in MetaCoq.PCUIC.Bidirectional.BDTyping]
infering_indu_size [in MetaCoq.PCUIC.Bidirectional.BDTyping]
infering_prod_size [in MetaCoq.PCUIC.Bidirectional.BDTyping]
infering_sort_size [in MetaCoq.PCUIC.Bidirectional.BDTyping]
infering_size [in MetaCoq.PCUIC.Bidirectional.BDTyping]
infer_and_print_template_program_with_guard [in MetaCoq.SafeChecker.Extraction]
infer_sorting [in MetaCoq.Template.Typing]
infer_as_prod [in MetaCoq.SafeChecker.PCUICSafeRetyping]
infer_as_sort [in MetaCoq.SafeChecker.PCUICSafeRetyping]
infer_and_print_template_program [in MetaCoq.SafeChecker.SafeTemplateChecker]
infer_template_program [in MetaCoq.SafeChecker.SafeTemplateChecker]
infer_term [in MetaCoq.Template.Checker]
infer_cumul [in MetaCoq.Template.Checker]
infer_type [in MetaCoq.Template.Checker]
infer_spine [in MetaCoq.Template.Checker]
infer_sorts_local_ctx [in MetaCoq.SafeChecker.PCUICSafeChecker]
infer_type_wf_env [in MetaCoq.SafeChecker.PCUICSafeChecker]
infer_wf_env [in MetaCoq.SafeChecker.PCUICSafeChecker]
infer_typing [in MetaCoq.SafeChecker.PCUICSafeChecker]
infer_term [in MetaCoq.SafeChecker.PCUICSafeChecker]
infer_isType [in MetaCoq.SafeChecker.PCUICTypeChecker]
infer_type [in MetaCoq.SafeChecker.PCUICTypeChecker]
infer' [in MetaCoq.Template.Checker]
Informative [in MetaCoq.PCUIC.PCUICElimination]
inh [in MetaCoq.Examples.typing_correctness]
inh [in MetaCoq.Examples.metacoq_tour_prelude]
inhabit_formula [in MetaCoq.Examples.tauto]
init_env [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
init_graph [in MetaCoq.Template.common.uGraph]
inj_open [in MetaCoq.PCUIC.PCUICContextConversion]
inj_closed [in MetaCoq.PCUIC.PCUICContextConversion]
inline_projections_optimization [in MetaCoq.Erasure.ETransform]
inspect [in MetaCoq.Erasure.ErasureFunction]
inspect [in MetaCoq.SafeChecker.PCUICSafeReduce]
inspect [in MetaCoq.Examples.tauto]
inspect [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
inspect_bool [in MetaCoq.Erasure.ErasureFunction]
inst [in MetaCoq.PCUIC.PCUICSigmaCalculus]
Instance.empty [in MetaCoq.Template.Universes]
Instance.eqb [in MetaCoq.Template.Universes]
Instance.equal_upto [in MetaCoq.Template.Universes]
Instance.is_empty [in MetaCoq.Template.Universes]
Instance.t [in MetaCoq.Template.Universes]
instantiate_params_subst [in MetaCoq.Template.Typing]
inst_case_context [in MetaCoq.Template.Ast]
inst_case_branch_context [in MetaCoq.PCUIC.Syntax.PCUICCases]
inst_case_predicate_context [in MetaCoq.PCUIC.Syntax.PCUICCases]
inst_case_context [in MetaCoq.PCUIC.Syntax.PCUICCases]
inst_telescope [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_constructor_body [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
inst_mutual_inductive_body [in MetaCoq.PCUIC.Syntax.PCUICInstDef]
inst_context_snoc0 [in MetaCoq.PCUIC.Syntax.PCUICInstDef]
inst_decl [in MetaCoq.PCUIC.Syntax.PCUICInstDef]
inst_context [in MetaCoq.PCUIC.Syntax.PCUICInstDef]
inverse [in MetaCoq.Translations.MiniHoTT]
inverse [in MetaCoq.Translations.MiniHoTT_paths]
inverse_ap [in MetaCoq.Translations.MiniHoTT]
inverse_ap [in MetaCoq.Translations.MiniHoTT_paths]
inverse2 [in MetaCoq.Translations.MiniHoTT]
inverse2 [in MetaCoq.Translations.MiniHoTT_paths]
inv_V [in MetaCoq.Translations.MiniHoTT]
inv_VV [in MetaCoq.Translations.MiniHoTT]
inv_pV [in MetaCoq.Translations.MiniHoTT]
inv_Vp [in MetaCoq.Translations.MiniHoTT]
inv_pp [in MetaCoq.Translations.MiniHoTT]
inv_V [in MetaCoq.Translations.MiniHoTT_paths]
inv_VV [in MetaCoq.Translations.MiniHoTT_paths]
inv_pV [in MetaCoq.Translations.MiniHoTT_paths]
inv_Vp [in MetaCoq.Translations.MiniHoTT_paths]
inv_pp [in MetaCoq.Translations.MiniHoTT_paths]
iota_red [in MetaCoq.Template.Typing]
iota_red [in MetaCoq.PCUIC.Syntax.PCUICCases]
iota_red [in MetaCoq.Erasure.EGlobalEnv]
isApp [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
isApp [in MetaCoq.Template.Ast]
isApp [in MetaCoq.PCUIC.PCUICAst]
isApp [in MetaCoq.Erasure.EAst]
isAppProd [in MetaCoq.PCUIC.PCUICSafeLemmata]
isArity [in MetaCoq.Template.Typing]
isArity [in MetaCoq.PCUIC.PCUICTyping]
isArityHead [in MetaCoq.PCUIC.PCUICWcbvEval]
isArityHead [in MetaCoq.Template.WcbvEval]
isAssRel [in MetaCoq.PCUIC.PCUICWcbvEval]
isAssRel [in MetaCoq.Template.WcbvEval]
isAxiom [in MetaCoq.PCUIC.PCUICWcbvEval]
isAxiom [in MetaCoq.Template.WcbvEval]
isBox [in MetaCoq.Erasure.EAstUtils]
isCoFinite [in MetaCoq.Template.Typing]
isCoFinite [in MetaCoq.PCUIC.PCUICTyping]
isCoFix [in MetaCoq.PCUIC.PCUICWcbvEval]
isCoFix [in MetaCoq.Template.Checker]
isCoFix [in MetaCoq.Template.WcbvEval]
isCoFix [in MetaCoq.Erasure.EAstUtils]
isCoFix_app [in MetaCoq.SafeChecker.PCUICSafeReduce]
isConstruct [in MetaCoq.Template.EtaExpand]
isConstruct [in MetaCoq.PCUIC.PCUICWcbvEval]
isConstruct [in MetaCoq.PCUIC.PCUICEtaExpand]
isConstruct [in MetaCoq.Template.Checker]
isConstruct [in MetaCoq.Template.WcbvEval]
isConstruct [in MetaCoq.Erasure.EAstUtils]
isConstructApp [in MetaCoq.PCUIC.PCUICWcbvEval]
isConstructApp [in MetaCoq.Template.WcbvEval]
isConstructApp [in MetaCoq.Erasure.EAstUtils]
isConstruct_app [in MetaCoq.PCUIC.utils.PCUICAstUtils]
isConstruct_app [in MetaCoq.Template.AstUtils]
isconv [in MetaCoq.SafeChecker.PCUICSafeConversion]
isconv [in MetaCoq.Template.Checker]
isconv_term [in MetaCoq.SafeChecker.PCUICSafeConversion]
isconv_full [in MetaCoq.SafeChecker.PCUICSafeConversion]
isconv_predicate [in MetaCoq.SafeChecker.PCUICSafeConversion]
isconv_predicate_params [in MetaCoq.SafeChecker.PCUICSafeConversion]
isconv_predicate_params_aux [in MetaCoq.SafeChecker.PCUICSafeConversion]
isconv_branches' [in MetaCoq.SafeChecker.PCUICSafeConversion]
isconv_branches [in MetaCoq.SafeChecker.PCUICSafeConversion]
isconv_context [in MetaCoq.SafeChecker.PCUICSafeConversion]
isconv_context_aux [in MetaCoq.SafeChecker.PCUICSafeConversion]
isconv_prog [in MetaCoq.Template.Checker]
isequiv [in MetaCoq.Translations.times_bool_fun2]
isequiv_eqᵗ_eq [in MetaCoq.Translations.times_bool_fun]
isequiv_moveR_V1 [in MetaCoq.Translations.MiniHoTT]
isequiv_moveR_1V [in MetaCoq.Translations.MiniHoTT]
isequiv_moveR_1M [in MetaCoq.Translations.MiniHoTT]
isequiv_moveR_M1 [in MetaCoq.Translations.MiniHoTT]
isequiv_moveL_V1 [in MetaCoq.Translations.MiniHoTT]
isequiv_moveL_1V [in MetaCoq.Translations.MiniHoTT]
isequiv_moveL_M1 [in MetaCoq.Translations.MiniHoTT]
isequiv_moveL_1M [in MetaCoq.Translations.MiniHoTT]
isequiv_moveL_pM [in MetaCoq.Translations.MiniHoTT]
isequiv_cancelR [in MetaCoq.Translations.MiniHoTT]
isequiv_cancelL [in MetaCoq.Translations.MiniHoTT]
isequiv_isequiv_precompose [in MetaCoq.Translations.MiniHoTT]
isequiv_involution [in MetaCoq.Translations.MiniHoTT]
isequiv_adjointify [in MetaCoq.Translations.MiniHoTT]
isequiv_commsq' [in MetaCoq.Translations.MiniHoTT]
isequiv_commsq [in MetaCoq.Translations.MiniHoTT]
isequiv_homotopic [in MetaCoq.Translations.MiniHoTT]
isequiv_compose' [in MetaCoq.Translations.MiniHoTT]
isequiv_moveR_V1 [in MetaCoq.Translations.MiniHoTT_paths]
isequiv_moveR_1V [in MetaCoq.Translations.MiniHoTT_paths]
isequiv_moveR_1M [in MetaCoq.Translations.MiniHoTT_paths]
isequiv_moveR_M1 [in MetaCoq.Translations.MiniHoTT_paths]
isequiv_moveL_V1 [in MetaCoq.Translations.MiniHoTT_paths]
isequiv_moveL_1V [in MetaCoq.Translations.MiniHoTT_paths]
isequiv_moveL_M1 [in MetaCoq.Translations.MiniHoTT_paths]
isequiv_moveL_1M [in MetaCoq.Translations.MiniHoTT_paths]
isequiv_moveL_pM [in MetaCoq.Translations.MiniHoTT_paths]
isequiv_cancelR [in MetaCoq.Translations.MiniHoTT_paths]
isequiv_cancelL [in MetaCoq.Translations.MiniHoTT_paths]
isequiv_isequiv_precompose [in MetaCoq.Translations.MiniHoTT_paths]
isequiv_involution [in MetaCoq.Translations.MiniHoTT_paths]
isequiv_adjointify [in MetaCoq.Translations.MiniHoTT_paths]
isequiv_commsq' [in MetaCoq.Translations.MiniHoTT_paths]
isequiv_commsq [in MetaCoq.Translations.MiniHoTT_paths]
isequiv_homotopic [in MetaCoq.Translations.MiniHoTT_paths]
isequiv_compose' [in MetaCoq.Translations.MiniHoTT_paths]
isErasable [in MetaCoq.Erasure.Extract]
isErasable_Type [in MetaCoq.Erasure.EArities]
isEtaExp [in MetaCoq.Erasure.EEtaExpandedFix]
isEtaExp [in MetaCoq.Erasure.EEtaExpanded]
isEtaExp_env [in MetaCoq.Erasure.EEtaExpandedFix]
isEtaExp_decl [in MetaCoq.Erasure.EEtaExpandedFix]
isEtaExp_constant_decl [in MetaCoq.Erasure.EEtaExpandedFix]
isEtaExp_fixapp [in MetaCoq.Erasure.EEtaExpandedFix]
isEtaExp_app [in MetaCoq.Erasure.EEtaExpandedFix]
isEtaExp_env [in MetaCoq.Erasure.EEtaExpanded]
isEtaExp_decl [in MetaCoq.Erasure.EEtaExpanded]
isEtaExp_constant_decl [in MetaCoq.Erasure.EEtaExpanded]
isEtaExp_app [in MetaCoq.Erasure.EEtaExpanded]
isEvar [in MetaCoq.PCUIC.PCUICWcbvEval]
isEvar [in MetaCoq.Template.WcbvEval]
isEvar [in MetaCoq.Erasure.EAstUtils]
isFinite [in MetaCoq.Template.Typing]
isFinite [in MetaCoq.PCUIC.PCUICTyping]
isFix [in MetaCoq.Template.EtaExpand]
isFix [in MetaCoq.PCUIC.PCUICWcbvEval]
isFix [in MetaCoq.PCUIC.PCUICEtaExpand]
isFix [in MetaCoq.Template.WcbvEval]
isFix [in MetaCoq.Erasure.EAstUtils]
isFixApp [in MetaCoq.PCUIC.PCUICWcbvEval]
isFixApp [in MetaCoq.Template.WcbvEval]
isFixApp [in MetaCoq.PCUIC.PCUICConversion]
isFixApp [in MetaCoq.Erasure.EAstUtils]
isFixLambda [in MetaCoq.PCUIC.Syntax.PCUICViews]
isFixLambda_app [in MetaCoq.PCUIC.Syntax.PCUICViews]
isFix_app [in MetaCoq.Template.EtaExpand]
isInd [in MetaCoq.PCUIC.utils.PCUICAstUtils]
isInd [in MetaCoq.PCUIC.PCUICWcbvEval]
isIndConstructApp [in MetaCoq.PCUIC.PCUICConvCumInversion]
isLambda [in MetaCoq.Template.Ast]
isLambda [in MetaCoq.PCUIC.PCUICAst]
isLambda [in MetaCoq.Erasure.EAst]
isProd [in MetaCoq.PCUIC.utils.PCUICAstUtils]
isPropositional [in MetaCoq.Erasure.Extract]
isPropositional [in MetaCoq.PCUIC.PCUICFirstorder]
isPropositionalArity [in MetaCoq.Erasure.Extract]
isred [in MetaCoq.SafeChecker.PCUICSafeReduce]
isred_full [in MetaCoq.SafeChecker.PCUICSafeConversion]
isRel [in MetaCoq.Template.EtaExpand]
isRel [in MetaCoq.PCUIC.PCUICEtaExpand]
isRel [in MetaCoq.Erasure.EAstUtils]
isRel [in MetaCoq.SafeChecker.PCUICSafeChecker]
isRel_app [in MetaCoq.Template.EtaExpand]
isRel_n [in MetaCoq.SafeChecker.PCUICSafeChecker]
isSome [in MetaCoq.Erasure.EWellformed]
isSort [in MetaCoq.PCUIC.utils.PCUICAstUtils]
isSort [in MetaCoq.Template.Typing]
isStackApp [in MetaCoq.PCUIC.Syntax.PCUICPosition]
isStuckFix [in MetaCoq.PCUIC.PCUICWcbvEval]
isStuckFix [in MetaCoq.Template.WcbvEval]
isStuckFix [in MetaCoq.Erasure.EWcbvEval]
isStuckFix' [in MetaCoq.Erasure.EEtaExpandedFix]
isType_welltyped [in MetaCoq.PCUIC.PCUICTyping]
isWfArity [in MetaCoq.PCUIC.PCUICTyping]
isws_cumul_pb_Fix [in MetaCoq.SafeChecker.PCUICSafeConversion]
isws_cumul_pb_fix_bodies [in MetaCoq.SafeChecker.PCUICSafeConversion]
isws_cumul_pb_fix_types [in MetaCoq.SafeChecker.PCUICSafeConversion]
is_allowed_elimination [in MetaCoq.Template.Universes]
is_lSet [in MetaCoq.Template.Universes]
is_declared_cstr_levels [in MetaCoq.Template.Universes]
is_propositional [in MetaCoq.Template.Universes]
is_allowed_elimination_cuniv [in MetaCoq.Template.Universes]
is_utype [in MetaCoq.Template.Universes]
is_uproplevel_or_set [in MetaCoq.Template.Universes]
is_uproplevel [in MetaCoq.Template.Universes]
is_usprop [in MetaCoq.Template.Universes]
is_uprop [in MetaCoq.Template.Universes]
Is_proof [in MetaCoq.PCUIC.PCUICElimination]
is_ind_app_head [in MetaCoq.PCUIC.utils.PCUICAstUtils]
is_cons [in MetaCoq.Erasure.EEtaExpandedFix]
is_nil [in MetaCoq.Erasure.EEtaExpandedFix]
is_suffix [in MetaCoq.Template.utils.MCList]
is_prefix [in MetaCoq.Template.utils.MCList]
is_fresh [in MetaCoq.Erasure.EPretty]
is_nil [in MetaCoq.Template.TemplateCheckWf]
is_constructor [in MetaCoq.Template.Typing]
is_axiom_decl [in MetaCoq.Erasure.Extract]
is_graph_of_uctx [in MetaCoq.Template.common.uGraph]
is_lt [in MetaCoq.Template.common.uGraph]
is_consistent [in MetaCoq.Template.common.uGraph]
is_constructor [in MetaCoq.PCUIC.Syntax.PCUICCases]
is_erasable [in MetaCoq.Erasure.ErasureFunction]
is_erasableb [in MetaCoq.Erasure.ErasureFunction]
is_arity [in MetaCoq.Erasure.ErasureFunction]
is_nil [in MetaCoq.Erasure.EWellformed]
is_graph_of_global_env_ext [in MetaCoq.Template.Checker]
is_leaf [in MetaCoq.Examples.tauto]
is_open_case [in MetaCoq.PCUIC.PCUICConversion]
Is_conv_to_Arity [in MetaCoq.PCUIC.PCUICConversion]
is_nth_constructor_app_or_box [in MetaCoq.Erasure.EGlobalEnv]
is_constructor_app_or_box [in MetaCoq.Erasure.EGlobalEnv]
is_nil [in MetaCoq.Erasure.EEtaExpanded]
is_box [in MetaCoq.Erasure.EAstUtils]
is_monomorphic_cstr [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
is_fresh [in MetaCoq.Template.Pretty]
is_ind_app_head [in MetaCoq.Template.AstUtils]
is_empty [in MetaCoq.Template.AstUtils]
is_fresh [in MetaCoq.PCUIC.utils.PCUICPretty]



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)