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)

A (definition)

aboveP [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
abstract_instance [in MetaCoq.Template.Universes]
abstract_env_ext_sq_wf [in MetaCoq.SafeChecker.PCUICWfEnv]
abstract_env_cored [in MetaCoq.SafeChecker.PCUICWfEnv]
abstract_env_impl [in MetaCoq.SafeChecker.PCUICWfEnv]
abstract_env_ext_impl [in MetaCoq.SafeChecker.PCUICWfEnv]
abstract_env_wf_universeb_correct [in MetaCoq.SafeChecker.PCUICWfEnv]
abstract_env_wf_universeb [in MetaCoq.SafeChecker.PCUICWfEnv]
abstract_env_leq [in MetaCoq.SafeChecker.PCUICWfEnv]
abstract_env_eq [in MetaCoq.SafeChecker.PCUICWfEnv]
abstract_conv_pb_relb [in MetaCoq.SafeChecker.PCUICSafeConversion]
abstract_env_ext_empty [in MetaCoq.SafeChecker.PCUICSafeChecker]
abstract_wf_cofixpoint [in MetaCoq.SafeChecker.PCUICTypeChecker]
abstract_wf_fixpoint [in MetaCoq.SafeChecker.PCUICTypeChecker]
abstract_check_recursivity_kind [in MetaCoq.SafeChecker.PCUICTypeChecker]
abstract_env_level_mem_forallb [in MetaCoq.SafeChecker.PCUICTypeChecker]
Acc_ind' [in MetaCoq.SafeChecker.PCUICSafeReduce]
Acc_equiv [in MetaCoq.SafeChecker.PCUICSafeReduce]
Acc_intro_generator [in MetaCoq.SafeChecker.PCUICSafeReduce]
add [in MetaCoq.Examples.demo]
addnP [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
add_global_decl [in MetaCoq.Translations.translation_utils]
add_uctx [in MetaCoq.Template.common.uGraph]
add_cstrs [in MetaCoq.Template.common.uGraph]
add_level_edges [in MetaCoq.Template.common.uGraph]
add_gc_of_constraint [in MetaCoq.Template.common.uGraph]
add_global_decl [in MetaCoq.PCUIC.TemplateToPCUIC]
add_suffix [in MetaCoq.Erasure.ErasureFunction]
add_gc_constraints [in MetaCoq.Template.Checker]
add_constructor [in MetaCoq.Examples.add_constructor]
add_ctor [in MetaCoq.Examples.add_constructor]
add' [in MetaCoq.Examples.demo]
alli [in MetaCoq.Template.utils.All_Forall]
alli_size [in MetaCoq.Template.utils.All_Forall]
allowed_eliminations_subset [in MetaCoq.Template.Universes]
All_rec [in MetaCoq.Erasure.EInduction]
All_over [in MetaCoq.Template.utils.All_Forall]
all_size [in MetaCoq.Template.utils.All_Forall]
all_env_flags_blocks [in MetaCoq.Erasure.EWellformed]
all_env_flags [in MetaCoq.Erasure.EWellformed]
all_term_flags [in MetaCoq.Erasure.EWellformed]
All_sigma [in MetaCoq.SafeChecker.PCUICSafeChecker]
all_rels [in MetaCoq.PCUIC.PCUICSpine]
all2i_size [in MetaCoq.Template.utils.All_Forall]
all2_size [in MetaCoq.Template.utils.All_Forall]
All2_map_right_inv [in MetaCoq.Template.utils.All_Forall]
All2_map_left_inv [in MetaCoq.Template.utils.All_Forall]
All2_prop2 [in MetaCoq.PCUIC.PCUICParallelReduction]
All2_prop2_eq [in MetaCoq.PCUIC.PCUICParallelReduction]
All2_prop [in MetaCoq.PCUIC.PCUICParallelReduction]
All2_prop_eq [in MetaCoq.PCUIC.PCUICParallelReduction]
All2_sq [in MetaCoq.SafeChecker.PCUICSafeChecker]
aname [in MetaCoq.Template.BasicAst]
and_assum [in MetaCoq.Template.utils.MCProd]
anon [in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
anonb [in MetaCoq.Examples.demo]
anonymize [in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
ap [in MetaCoq.Translations.MiniHoTT]
ap [in MetaCoq.Translations.MiniHoTT_paths]
apD [in MetaCoq.Translations.MiniHoTT]
apD [in MetaCoq.Translations.MiniHoTT_paths]
apD_transport_forall_constant [in MetaCoq.Translations.MiniHoTT]
apD_V [in MetaCoq.Translations.MiniHoTT]
apD_pp [in MetaCoq.Translations.MiniHoTT]
apD_1 [in MetaCoq.Translations.MiniHoTT]
apD_transport_forall_constant [in MetaCoq.Translations.MiniHoTT_paths]
apD_V [in MetaCoq.Translations.MiniHoTT_paths]
apD_pp [in MetaCoq.Translations.MiniHoTT_paths]
apD_1 [in MetaCoq.Translations.MiniHoTT_paths]
apD011 [in MetaCoq.Translations.MiniHoTT]
apD011 [in MetaCoq.Translations.MiniHoTT_paths]
apD02 [in MetaCoq.Translations.MiniHoTT]
apD02 [in MetaCoq.Translations.MiniHoTT_paths]
apD02_pp [in MetaCoq.Translations.MiniHoTT]
apD02_const [in MetaCoq.Translations.MiniHoTT]
apD02_pp [in MetaCoq.Translations.MiniHoTT_paths]
apD02_const [in MetaCoq.Translations.MiniHoTT_paths]
apD10 [in MetaCoq.Translations.MiniHoTT]
apD10 [in MetaCoq.Translations.MiniHoTT_paths]
apD10_path_forall [in MetaCoq.Translations.MiniHoTT]
apD10_ap_postcompose [in MetaCoq.Translations.MiniHoTT]
apD10_ap_precompose [in MetaCoq.Translations.MiniHoTT]
apD10_V [in MetaCoq.Translations.MiniHoTT]
apD10_pp [in MetaCoq.Translations.MiniHoTT]
apD10_1 [in MetaCoq.Translations.MiniHoTT]
apD10_path_forall [in MetaCoq.Translations.MiniHoTT_paths]
apD10_ap_postcompose [in MetaCoq.Translations.MiniHoTT_paths]
apD10_ap_precompose [in MetaCoq.Translations.MiniHoTT_paths]
apD10_V [in MetaCoq.Translations.MiniHoTT_paths]
apD10_pp [in MetaCoq.Translations.MiniHoTT_paths]
apD10_1 [in MetaCoq.Translations.MiniHoTT_paths]
application_atom [in MetaCoq.PCUIC.utils.PCUICAstUtils]
apply [in MetaCoq.Translations.param_binary]
appstack [in MetaCoq.PCUIC.Syntax.PCUICPosition]
ap_functor_sigma [in MetaCoq.Translations.MiniHoTT]
ap_existT [in MetaCoq.Translations.MiniHoTT]
ap_pr1_path_sigma [in MetaCoq.Translations.MiniHoTT]
ap_functor_forall [in MetaCoq.Translations.MiniHoTT]
ap_lambdaD [in MetaCoq.Translations.MiniHoTT]
ap_apply_lD2 [in MetaCoq.Translations.MiniHoTT]
ap_apply_lD [in MetaCoq.Translations.MiniHoTT]
ap_pr1_path_basedpaths' [in MetaCoq.Translations.MiniHoTT]
ap_pr1_path_basedpaths [in MetaCoq.Translations.MiniHoTT]
ap_pr1_path_contr_basedpaths' [in MetaCoq.Translations.MiniHoTT]
ap_pr1_path_contr_basedpaths [in MetaCoq.Translations.MiniHoTT]
ap_transport_pV_idmap [in MetaCoq.Translations.MiniHoTT]
ap_transport_Vp_idmap [in MetaCoq.Translations.MiniHoTT]
ap_transport_transport_pV [in MetaCoq.Translations.MiniHoTT]
ap_const [in MetaCoq.Translations.MiniHoTT]
ap_compose' [in MetaCoq.Translations.MiniHoTT]
ap_compose [in MetaCoq.Translations.MiniHoTT]
ap_idmap [in MetaCoq.Translations.MiniHoTT]
ap_V [in MetaCoq.Translations.MiniHoTT]
ap_pp_p [in MetaCoq.Translations.MiniHoTT]
ap_p_pp [in MetaCoq.Translations.MiniHoTT]
ap_pp [in MetaCoq.Translations.MiniHoTT]
ap_1 [in MetaCoq.Translations.MiniHoTT]
ap_functor_sigma [in MetaCoq.Translations.MiniHoTT_paths]
ap_existT [in MetaCoq.Translations.MiniHoTT_paths]
ap_pr1_path_sigma [in MetaCoq.Translations.MiniHoTT_paths]
ap_functor_forall [in MetaCoq.Translations.MiniHoTT_paths]
ap_lambdaD [in MetaCoq.Translations.MiniHoTT_paths]
ap_apply_lD2 [in MetaCoq.Translations.MiniHoTT_paths]
ap_apply_lD [in MetaCoq.Translations.MiniHoTT_paths]
ap_pr1_path_basedpaths' [in MetaCoq.Translations.MiniHoTT_paths]
ap_pr1_path_basedpaths [in MetaCoq.Translations.MiniHoTT_paths]
ap_pr1_path_contr_basedpaths' [in MetaCoq.Translations.MiniHoTT_paths]
ap_pr1_path_contr_basedpaths [in MetaCoq.Translations.MiniHoTT_paths]
ap_transport_pV_idmap [in MetaCoq.Translations.MiniHoTT_paths]
ap_transport_Vp_idmap [in MetaCoq.Translations.MiniHoTT_paths]
ap_transport_transport_pV [in MetaCoq.Translations.MiniHoTT_paths]
ap_const [in MetaCoq.Translations.MiniHoTT_paths]
ap_compose' [in MetaCoq.Translations.MiniHoTT_paths]
ap_compose [in MetaCoq.Translations.MiniHoTT_paths]
ap_idmap [in MetaCoq.Translations.MiniHoTT_paths]
ap_V [in MetaCoq.Translations.MiniHoTT_paths]
ap_pp_p [in MetaCoq.Translations.MiniHoTT_paths]
ap_p_pp [in MetaCoq.Translations.MiniHoTT_paths]
ap_pp [in MetaCoq.Translations.MiniHoTT_paths]
ap_1 [in MetaCoq.Translations.MiniHoTT_paths]
ap01D1 [in MetaCoq.Translations.MiniHoTT]
ap01D1 [in MetaCoq.Translations.MiniHoTT_paths]
ap011 [in MetaCoq.Translations.MiniHoTT]
ap011 [in MetaCoq.Translations.MiniHoTT_paths]
ap011D [in MetaCoq.Translations.MiniHoTT]
ap011D [in MetaCoq.Translations.MiniHoTT_paths]
ap02 [in MetaCoq.Translations.MiniHoTT]
ap02 [in MetaCoq.Translations.MiniHoTT_paths]
ap02_p2p [in MetaCoq.Translations.MiniHoTT]
ap02_pp [in MetaCoq.Translations.MiniHoTT]
ap02_p2p [in MetaCoq.Translations.MiniHoTT_paths]
ap02_pp [in MetaCoq.Translations.MiniHoTT_paths]
ap10 [in MetaCoq.Translations.MiniHoTT]
ap10 [in MetaCoq.Translations.MiniHoTT_paths]
ap10_ap_postcompose [in MetaCoq.Translations.MiniHoTT]
ap10_ap_precompose [in MetaCoq.Translations.MiniHoTT]
ap10_V [in MetaCoq.Translations.MiniHoTT]
ap10_pp [in MetaCoq.Translations.MiniHoTT]
ap10_1 [in MetaCoq.Translations.MiniHoTT]
ap10_equiv [in MetaCoq.Translations.MiniHoTT]
ap10_ap_postcompose [in MetaCoq.Translations.MiniHoTT_paths]
ap10_ap_precompose [in MetaCoq.Translations.MiniHoTT_paths]
ap10_V [in MetaCoq.Translations.MiniHoTT_paths]
ap10_pp [in MetaCoq.Translations.MiniHoTT_paths]
ap10_1 [in MetaCoq.Translations.MiniHoTT_paths]
ap10_equiv [in MetaCoq.Translations.MiniHoTT_paths]
ap11 [in MetaCoq.Translations.MiniHoTT]
ap11 [in MetaCoq.Translations.MiniHoTT_paths]
ap11_is_ap10_ap01 [in MetaCoq.Translations.MiniHoTT]
ap11_is_ap10_ap01 [in MetaCoq.Translations.MiniHoTT_paths]
arguments [in MetaCoq.PCUIC.utils.PCUICAstUtils]
arity_ass_context [in MetaCoq.SafeChecker.PCUICSafeReduce]
arity_ass [in MetaCoq.SafeChecker.PCUICSafeReduce]
atom [in MetaCoq.PCUIC.PCUICWcbvEval]
atom [in MetaCoq.Template.WcbvEval]
atom [in MetaCoq.Erasure.EWcbvEval]
atom [in MetaCoq.PCUIC.PCUICReduction]
atomic_term [in MetaCoq.Erasure.EWcbvEvalEtaInd]
atpos [in MetaCoq.PCUIC.Syntax.PCUICPosition]
AUContext.inter [in MetaCoq.Template.Universes]
AUContext.levels [in MetaCoq.Template.Universes]
AUContext.make [in MetaCoq.Template.Universes]
AUContext.repr [in MetaCoq.Template.Universes]
AUContext.t [in MetaCoq.Template.Universes]
Aux [in MetaCoq.SafeChecker.PCUICSafeConversion]
Aux' [in MetaCoq.SafeChecker.PCUICSafeConversion]
axiom_free [in MetaCoq.PCUIC.PCUICProgress]
axiom_free [in MetaCoq.Erasure.Extract]
axiom_free [in MetaCoq.SafeChecker.PCUICConsistency]
axiom_free_value [in MetaCoq.PCUIC.PCUICCanonicity]


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)