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 (definition)

gcs_levels_declared [in MetaCoq.Template.common.uGraph]
gcs_equal [in MetaCoq.Template.common.uGraph]
gcs_equal [in MetaCoq.SafeChecker.PCUICSafeChecker]
gctx [in MetaCoq.Examples.typing_correctness]
gctx [in MetaCoq.Examples.metacoq_tour_prelude]
gctx_wf_env [in MetaCoq.Examples.typing_correctness]
gctx_union [in MetaCoq.Template.common.uGraph]
gctx_wf_env [in MetaCoq.Examples.metacoq_tour_prelude]
gc_result_eq [in MetaCoq.Template.common.uGraph]
gc_levels_declared' [in MetaCoq.Template.common.uGraph]
gc_eq_universe [in MetaCoq.Template.common.uGraph]
gc_leq_universe [in MetaCoq.Template.common.uGraph]
gc_levels_declared_univ [in MetaCoq.Template.common.uGraph]
gc_levels_declared [in MetaCoq.Template.common.uGraph]
gc_expr_declared [in MetaCoq.Template.common.uGraph]
gc_level_declared [in MetaCoq.Template.common.uGraph]
gc_of_uctx [in MetaCoq.Template.common.uGraph]
gc_lt_levelalg [in MetaCoq.Template.common.uGraph]
gc_leq_levelalg [in MetaCoq.Template.common.uGraph]
gc_lt0_levelalg [in MetaCoq.Template.common.uGraph]
gc_leq0_levelalg [in MetaCoq.Template.common.uGraph]
gc_eq_levelalg [in MetaCoq.Template.common.uGraph]
gc_eq0_levelalg [in MetaCoq.Template.common.uGraph]
gc_leq_levelalg_n [in MetaCoq.Template.common.uGraph]
gc_leq0_levelalg_n [in MetaCoq.Template.common.uGraph]
gc_of_constraints [in MetaCoq.Template.common.uGraph]
gc_of_constraint [in MetaCoq.Template.common.uGraph]
gc_consistent [in MetaCoq.Template.common.uGraph]
gc_satisfies [in MetaCoq.Template.common.uGraph]
gen_transform_env' [in MetaCoq.Erasure.EGenericMapEnv]
gen_transform_env [in MetaCoq.Erasure.EGenericMapEnv]
gen_transform_decl [in MetaCoq.Erasure.EGenericMapEnv]
gen_transform_constant_decl [in MetaCoq.Erasure.EGenericMapEnv]
GlobalContextMap.constructor_isprop_pars_decl [in MetaCoq.Erasure.EEnvMap]
GlobalContextMap.inductive_isprop_and_pars [in MetaCoq.Erasure.EEnvMap]
GlobalContextMap.lookup_inductive_pars [in MetaCoq.Erasure.EEnvMap]
GlobalContextMap.lookup_projection [in MetaCoq.Erasure.EEnvMap]
GlobalContextMap.lookup_constructor [in MetaCoq.Erasure.EEnvMap]
GlobalContextMap.lookup_inductive [in MetaCoq.Erasure.EEnvMap]
GlobalContextMap.lookup_minductive [in MetaCoq.Erasure.EEnvMap]
GlobalContextMap.lookup_env [in MetaCoq.Erasure.EEnvMap]
GlobalContextMap.make [in MetaCoq.Erasure.EEnvMap]
GlobalMaps.check_ind_sorts [in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.check_constructors_smaller [in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.constructor_univs [in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.cstr_concl [in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.cstr_concl_head [in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.cstr_respects_variance [in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.elim_sort_sprop_ind [in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.elim_sort_prop_ind [in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.fresh_global [in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.ind_respects_variance [in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.ind_arities [in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.ind_realargs [in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.level_var_instance [in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.lift_constraints [in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.lift_constraint [in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.lift_instance [in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.lift_level [in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.on_global_env_ext [in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.on_global_env [in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.on_global_univs [in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.on_global_decl [in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.on_constant_decl [in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.on_variance [in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.on_projection [in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.on_constructors [in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.on_udecl [in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.on_type [in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.on_context [in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.satisfiable_udecl [in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.sorts_local_ctx [in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.type_local_ctx [in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.univs_ext_constraints [in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.valid_on_mono_udecl [in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.variance_universes [in MetaCoq.Template.EnvironmentTyping]
GlobalMaps.variance_cstrs [in MetaCoq.Template.EnvironmentTyping]
globals_erased_with_deps [in MetaCoq.Erasure.EDeps]
global_variance [in MetaCoq.Template.TermEquality]
global_gc_uctx_invariants [in MetaCoq.Template.common.uGraph]
global_uctx_invariants [in MetaCoq.Template.common.uGraph]
global_variance [in MetaCoq.PCUIC.PCUICEquality]
global_env_add [in MetaCoq.SafeChecker.PCUICConsistency]
global_erased_with_deps [in MetaCoq.Erasure.ErasureFunction]
global_declarations [in MetaCoq.Erasure.EAst]
global_ext_uctx_consistent [in MetaCoq.PCUIC.PCUICGlobalEnv]
global_declarations_size [in MetaCoq.PCUIC.PCUICTyping]
global_subset [in MetaCoq.Erasure.EExtends]
global_env_ext_map_global_env_map [in MetaCoq.PCUIC.PCUICProgram]
global_env_ext_map_global_env_ext [in MetaCoq.PCUIC.PCUICProgram]
global_env_ext_map [in MetaCoq.PCUIC.PCUICProgram]
global_context_set [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
global_ext_context_set [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
global_uctx_univs [in MetaCoq.SafeChecker.PCUICSafeChecker]
globdecls_size [in MetaCoq.Template.Typing]
globenv_size [in MetaCoq.Template.Typing]
globenv_size [in MetaCoq.PCUIC.PCUICTyping]
GoodConstraintSet_pair [in MetaCoq.Template.common.uGraph]
GoodConstraint.compare [in MetaCoq.Template.common.uGraph]
GoodConstraint.eq [in MetaCoq.Template.common.uGraph]
GoodConstraint.eq_dec [in MetaCoq.Template.common.uGraph]
GoodConstraint.eq_equiv [in MetaCoq.Template.common.uGraph]
GoodConstraint.eq_trans [in MetaCoq.Template.common.uGraph]
GoodConstraint.eq_sym [in MetaCoq.Template.common.uGraph]
GoodConstraint.eq_refl [in MetaCoq.Template.common.uGraph]
GoodConstraint.lt [in MetaCoq.Template.common.uGraph]
GoodConstraint.satisfies [in MetaCoq.Template.common.uGraph]
GoodConstraint.t [in MetaCoq.Template.common.uGraph]
gref_eq_dec [in MetaCoq.Template.Kernames]
gref_eqb [in MetaCoq.Template.Kernames]
guarded_to_unguarded_fix [in MetaCoq.Erasure.ETransform]



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)