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)

L (definition)

labelling_of_valuation [in MetaCoq.Template.common.uGraph]
lengths [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
lengths [in MetaCoq.PCUIC.Syntax.PCUICTactics]
leqb_universe_n_ [in MetaCoq.Template.Universes]
leqb_universe [in MetaCoq.Template.common.uGraph]
leqb_levelalg_n [in MetaCoq.Template.common.uGraph]
leqb_expr_univ_n [in MetaCoq.Template.common.uGraph]
leqb_expr_n [in MetaCoq.Template.common.uGraph]
leqb_level_n [in MetaCoq.Template.common.uGraph]
leqb_term [in MetaCoq.SafeChecker.PCUICEqualityDec]
leq_universe_refl' [in MetaCoq.Template.Universes]
leq_universe [in MetaCoq.Template.Universes]
leq_levelalg [in MetaCoq.Template.Universes]
leq_universe_n [in MetaCoq.Template.Universes]
leq_universe_n_ [in MetaCoq.Template.Universes]
leq_levelalg_n [in MetaCoq.Template.Universes]
leq_cuniverse [in MetaCoq.Template.Universes]
leq_cuniverse_n [in MetaCoq.Template.Universes]
leq_term_ext [in MetaCoq.PCUIC.PCUICCumulativity]
leq_term_nocast [in MetaCoq.Template.Typing]
leq_term [in MetaCoq.Template.Checker]
leq0_levelalg_n [in MetaCoq.Template.Universes]
leq0_level_n [in MetaCoq.Template.common.uGraph]
let_expansion_obseq [in MetaCoq.PCUIC.PCUICTransform]
LevelAlgExpr.exprs [in MetaCoq.Template.Universes]
LevelAlgExpr.get_is_level [in MetaCoq.Template.Universes]
LevelAlgExpr.is_level [in MetaCoq.Template.Universes]
LevelAlgExpr.is_levels [in MetaCoq.Template.Universes]
LevelAlgExpr.make [in MetaCoq.Template.Universes]
LevelAlgExpr.make' [in MetaCoq.Template.Universes]
LevelAlgExpr.succ [in MetaCoq.Template.Universes]
LevelAlgExpr.sup [in MetaCoq.Template.Universes]
LevelAlgExpr.t [in MetaCoq.Template.Universes]
LevelExpr.compare [in MetaCoq.Template.Universes]
LevelExpr.compare_spec [in MetaCoq.Template.Universes]
LevelExpr.eq [in MetaCoq.Template.Universes]
LevelExpr.eq_leibniz [in MetaCoq.Template.Universes]
LevelExpr.eq_dec [in MetaCoq.Template.Universes]
LevelExpr.eq_equiv [in MetaCoq.Template.Universes]
LevelExpr.from_kernel_repr [in MetaCoq.Template.Universes]
LevelExpr.get_noprop [in MetaCoq.Template.Universes]
LevelExpr.get_level [in MetaCoq.Template.Universes]
LevelExpr.is_level [in MetaCoq.Template.Universes]
LevelExpr.lt [in MetaCoq.Template.Universes]
LevelExpr.lt_compat [in MetaCoq.Template.Universes]
LevelExpr.make [in MetaCoq.Template.Universes]
LevelExpr.set [in MetaCoq.Template.Universes]
LevelExpr.succ [in MetaCoq.Template.Universes]
LevelExpr.t [in MetaCoq.Template.Universes]
LevelExpr.to_kernel_repr [in MetaCoq.Template.Universes]
LevelExpr.type1 [in MetaCoq.Template.Universes]
LevelSetsUIP.eqb_LevelSet [in MetaCoq.Template.Reflect]
LevelSetsUIP.levels_tree_rect [in MetaCoq.Template.Reflect]
LevelSetsUIP.levels_tree_eqb [in MetaCoq.Template.Reflect]
LevelSet_mem_union [in MetaCoq.Template.Universes]
LevelSet_pair [in MetaCoq.Template.Universes]
levels_of_udecl [in MetaCoq.Template.Universes]
level_mem [in MetaCoq.SafeChecker.PCUICWfEnv]
level_lt_ind_dep [in MetaCoq.Template.Reflect]
Level.compare [in MetaCoq.Template.Universes]
Level.compare_spec [in MetaCoq.Template.Universes]
Level.eq [in MetaCoq.Template.Universes]
Level.eqb [in MetaCoq.Template.Universes]
Level.eq_dec [in MetaCoq.Template.Universes]
Level.eq_leibniz [in MetaCoq.Template.Universes]
Level.eq_level [in MetaCoq.Template.Universes]
Level.eq_equiv [in MetaCoq.Template.Universes]
Level.is_var [in MetaCoq.Template.Universes]
Level.is_set [in MetaCoq.Template.Universes]
Level.lt [in MetaCoq.Template.Universes]
Level.lt_compat [in MetaCoq.Template.Universes]
Level.lt_strorder [in MetaCoq.Template.Universes]
Level.t [in MetaCoq.Template.Universes]
lexprod [in MetaCoq.PCUIC.utils.PCUICUtils]
le_ind_prop [in MetaCoq.Template.Reflect]
lift [in MetaCoq.Template.Ast]
lift [in MetaCoq.PCUIC.PCUICAst]
lift [in MetaCoq.Erasure.ELiftSubst]
lift_ctx [in MetaCoq.Template.EtaExpand]
lift_renaming [in MetaCoq.PCUIC.PCUICSigmaCalculus]
lift_mutual_inductive_body [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
lift_ws [in MetaCoq.PCUIC.PCUICConfluence]
lift_context_snoc0 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
lift_context_snoc0 [in MetaCoq.Template.TypingWf]
ListOrderedType.compare [in MetaCoq.Template.utils.MCCompare]
ListOrderedType.compare_spec [in MetaCoq.Template.utils.MCCompare]
ListOrderedType.eq [in MetaCoq.Template.utils.MCCompare]
ListOrderedType.eqb [in MetaCoq.Template.utils.MCCompare]
ListOrderedType.eqb_dec [in MetaCoq.Template.utils.MCCompare]
ListOrderedType.eq_leibniz [in MetaCoq.Template.utils.MCCompare]
ListOrderedType.eq_equiv [in MetaCoq.Template.utils.MCCompare]
ListOrderedType.lt [in MetaCoq.Template.utils.MCCompare]
ListOrderedType.t [in MetaCoq.Template.utils.MCCompare]
list_size [in MetaCoq.Template.utils.MCList]
list_depth_gen [in MetaCoq.PCUIC.Syntax.PCUICDepth]
lookup [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
lookup_global_env [in MetaCoq.Template.EtaExpand]
lookup_tsl_table' [in MetaCoq.Translations.translation_utils]
lookup_tsl_table [in MetaCoq.Translations.translation_utils]
lookup_ind_decl [in MetaCoq.Erasure.EPretty]
lookup_wf_local_decl [in MetaCoq.Template.Typing]
lookup_wf_local [in MetaCoq.Template.Typing]
lookup_constructor [in MetaCoq.Template.TermEquality]
lookup_inductive [in MetaCoq.Template.TermEquality]
lookup_minductive [in MetaCoq.Template.TermEquality]
lookup_ind_decl [in MetaCoq.SafeChecker.PCUICSafeRetyping]
lookup_constant [in MetaCoq.Erasure.ErasureProperties]
lookup_env [in MetaCoq.Template.Checker]
lookup_constructor_type_cstrs [in MetaCoq.Template.Checker]
lookup_constructor_type [in MetaCoq.Template.Checker]
lookup_constructor_decl [in MetaCoq.Template.Checker]
lookup_ind_type_cstrs [in MetaCoq.Template.Checker]
lookup_ind_type [in MetaCoq.Template.Checker]
lookup_ind_decl [in MetaCoq.Template.Checker]
lookup_constant_type_cstrs [in MetaCoq.Template.Checker]
lookup_constant_type [in MetaCoq.Template.Checker]
lookup_wf_local_decl [in MetaCoq.PCUIC.PCUICTyping]
lookup_wf_local [in MetaCoq.PCUIC.PCUICTyping]
lookup_projection [in MetaCoq.Erasure.EGlobalEnv]
lookup_constructor_pars_args [in MetaCoq.Erasure.EGlobalEnv]
lookup_constructor [in MetaCoq.Erasure.EGlobalEnv]
lookup_inductive_pars [in MetaCoq.Erasure.EGlobalEnv]
lookup_inductive [in MetaCoq.Erasure.EGlobalEnv]
lookup_minductive [in MetaCoq.Erasure.EGlobalEnv]
lookup_constant [in MetaCoq.Erasure.EGlobalEnv]
lookup_env [in MetaCoq.Erasure.EGlobalEnv]
lookup_ind_decl [in MetaCoq.Template.Pretty]
lookup_inductive [in MetaCoq.Template.AstUtils]
lookup_minductive [in MetaCoq.Template.AstUtils]
lookup_mind_decl [in MetaCoq.Template.AstUtils]
lookup_ind_decl [in MetaCoq.PCUIC.utils.PCUICPretty]
lookup_ind_decl [in MetaCoq.SafeChecker.PCUICTypeChecker]
Lookup.consistent_instance_ext [in MetaCoq.Template.EnvironmentTyping]
Lookup.consistent_instance [in MetaCoq.Template.EnvironmentTyping]
Lookup.declared_projection [in MetaCoq.Template.EnvironmentTyping]
Lookup.declared_constructor [in MetaCoq.Template.EnvironmentTyping]
Lookup.declared_inductive [in MetaCoq.Template.EnvironmentTyping]
Lookup.declared_minductive [in MetaCoq.Template.EnvironmentTyping]
Lookup.declared_constant [in MetaCoq.Template.EnvironmentTyping]
Lookup.global_ext_uctx [in MetaCoq.Template.EnvironmentTyping]
Lookup.global_ext_constraints [in MetaCoq.Template.EnvironmentTyping]
Lookup.global_ext_levels [in MetaCoq.Template.EnvironmentTyping]
Lookup.global_uctx [in MetaCoq.Template.EnvironmentTyping]
Lookup.global_constraints [in MetaCoq.Template.EnvironmentTyping]
Lookup.global_levels [in MetaCoq.Template.EnvironmentTyping]
Lookup.lookup_projection [in MetaCoq.Template.EnvironmentTyping]
Lookup.lookup_constructor [in MetaCoq.Template.EnvironmentTyping]
Lookup.lookup_inductive [in MetaCoq.Template.EnvironmentTyping]
Lookup.lookup_minductive [in MetaCoq.Template.EnvironmentTyping]
Lookup.lookup_constant [in MetaCoq.Template.EnvironmentTyping]
Lookup.on_udecl_decl [in MetaCoq.Template.EnvironmentTyping]
Lookup.universes_decl_of_decl [in MetaCoq.Template.EnvironmentTyping]
Lookup.wf_universe [in MetaCoq.Template.EnvironmentTyping]
lsp_expr [in MetaCoq.Template.common.uGraph]
lt [in MetaCoq.Template.utils.ByteCompareSpec]
lt_universe [in MetaCoq.Template.Universes]
lt_levelalg [in MetaCoq.Template.Universes]
lt_cuniverse [in MetaCoq.Template.Universes]


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)