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)

G (lemma)

gcs_elements_union [in MetaCoq.Template.common.uGraph]
GCS_pair_spec [in MetaCoq.Template.common.uGraph]
gc_of_uctx_levels [in MetaCoq.Template.common.uGraph]
gc_of_uctx_union [in MetaCoq.Template.common.uGraph]
gc_of_constraints_union [in MetaCoq.Template.common.uGraph]
gc_of_constraintsP [in MetaCoq.Template.common.uGraph]
gc_of_constraints_declared [in MetaCoq.Template.common.uGraph]
gc_leq0_levelalg_n_sup [in MetaCoq.Template.common.uGraph]
gc_level_declared_make_graph [in MetaCoq.Template.common.uGraph]
gc_of_uctx_invariants [in MetaCoq.Template.common.uGraph]
gc_of_constraint_iff [in MetaCoq.Template.common.uGraph]
gc_of_constraints_of_uctx [in MetaCoq.Template.common.uGraph]
gc_of_uctx_of_constraints [in MetaCoq.Template.common.uGraph]
gc_eq_levelalg_iff [in MetaCoq.Template.common.uGraph]
gc_leq_levelalg_iff [in MetaCoq.Template.common.uGraph]
gc_leq_levelalg_n_iff [in MetaCoq.Template.common.uGraph]
gc_eq0_levelalg_iff [in MetaCoq.Template.common.uGraph]
gc_leq0_levelalg_iff [in MetaCoq.Template.common.uGraph]
gc_leq0_levelalg_n_iff [in MetaCoq.Template.common.uGraph]
gc_consistent_iff [in MetaCoq.Template.common.uGraph]
gc_of_constraints_spec [in MetaCoq.Template.common.uGraph]
gc_of_constraint_spec [in MetaCoq.Template.common.uGraph]
gc_satisfies_singleton [in MetaCoq.Template.common.uGraph]
gc_satisfies_pair [in MetaCoq.Template.common.uGraph]
gen_transform_env_wf [in MetaCoq.Erasure.EGenericMapEnv]
gen_transform_decl_wf [in MetaCoq.Erasure.EGenericMapEnv]
gen_transform_wellformed_decl_irrel [in MetaCoq.Erasure.EGenericMapEnv]
gen_transform_wellformed_irrel [in MetaCoq.Erasure.EGenericMapEnv]
gen_transform_env_eq [in MetaCoq.Erasure.EGenericMapEnv]
gen_transform_env_extends' [in MetaCoq.Erasure.EGenericMapEnv]
get_is_level_correct [in MetaCoq.Template.Universes]
get_level_make [in MetaCoq.SafeChecker.PCUICSafeConversion]
get_wt_indices [in MetaCoq.SafeChecker.PCUICSafeChecker]
GlobalContextMap.constructor_isprop_pars_decl_spec [in MetaCoq.Erasure.EEnvMap]
GlobalContextMap.inductive_isprop_and_pars_spec [in MetaCoq.Erasure.EEnvMap]
GlobalContextMap.lookup_inductive_pars_spec [in MetaCoq.Erasure.EEnvMap]
GlobalContextMap.lookup_projection_spec [in MetaCoq.Erasure.EEnvMap]
GlobalContextMap.lookup_constructor_spec [in MetaCoq.Erasure.EEnvMap]
GlobalContextMap.lookup_inductive_spec [in MetaCoq.Erasure.EEnvMap]
GlobalContextMap.lookup_minductive_spec [in MetaCoq.Erasure.EEnvMap]
GlobalContextMap.lookup_env_spec [in MetaCoq.Erasure.EEnvMap]
GlobalMaps.on_global_env_impl [in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.sorts_local_ctx_impl [in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.type_local_ctx_impl [in MetaCoq.Template.EnvironmentTyping]
global_levels_sub [in MetaCoq.PCUIC.PCUICWeakeningEnv]
global_levels_union_set [in MetaCoq.PCUIC.PCUICWeakeningEnv]
global_ext_constraints_app [in MetaCoq.PCUIC.PCUICWeakeningEnv]
global_ext_constraints_trans [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
global_ext_levels_trans [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
global_constraints_trans [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
global_levels_trans [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
global_variance_napp_mon [in MetaCoq.Template.TermEquality]
global_variance_sigma_mon [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
global_uctx_graph_invariants [in MetaCoq.Template.common.uGraph]
global_variance_empty [in MetaCoq.PCUIC.PCUICEquality]
global_variance_napp_mon [in MetaCoq.PCUIC.PCUICEquality]
global_erased_with_deps_weaken_prefix [in MetaCoq.Erasure.ErasureFunction]
global_env_ind [in MetaCoq.Erasure.ErasureFunction]
global_erases_with_deps_weaken [in MetaCoq.Erasure.ErasureFunction]
global_erases_with_deps_cons [in MetaCoq.Erasure.ErasureFunction]
global_ext_constraints_nlg [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
global_ext_levels_nlg [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
global_variance_nl_sigma_mon [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
global_subset_cons_right [in MetaCoq.Erasure.EExtends]
global_subset_cons [in MetaCoq.Erasure.EExtends]
global_subset_In [in MetaCoq.Erasure.EExtends]
global_context_set_sub_ext [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
global_uctx_invariants_ext [in MetaCoq.SafeChecker.PCUICTypeChecker]
GoodConstraintSet_pair_In [in MetaCoq.Template.common.uGraph]
GoodConstraint.compare_spec [in MetaCoq.Template.common.uGraph]
GoodConstraint.compare_refl [in MetaCoq.Template.common.uGraph]
GoodConstraint.compare_eq [in MetaCoq.Template.common.uGraph]
GoodConstraint.compare_trans [in MetaCoq.Template.common.uGraph]
GoodConstraint.compare_sym [in MetaCoq.Template.common.uGraph]
GoodConstraint.lt_compat [in MetaCoq.Template.common.uGraph]
GoodConstraint.lt_strorder [in MetaCoq.Template.common.uGraph]
GoodConstraint.lt_not_eq [in MetaCoq.Template.common.uGraph]
GoodConstraint.lt_trans [in MetaCoq.Template.common.uGraph]
GoodConstraint.nat_compare_eq [in MetaCoq.Template.common.uGraph]
GoodConstraint.nat_compare_trans [in MetaCoq.Template.common.uGraph]
GoodConstraint.Z_compare_trans [in MetaCoq.Template.common.uGraph]
graph_of_wf_ext [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
graph_of_wf [in MetaCoq.SafeChecker.PCUICWfEnvImpl]


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)