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)

U (definition)

UA [in MetaCoq.Translations.times_bool_fun]
UA [in MetaCoq.Translations.times_bool_fun2]
UA_postcomposeequiv' [in MetaCoq.Translations.times_bool_fun2]
UA_postcomposeequiv [in MetaCoq.Translations.times_bool_fun2]
UContext.constraints [in MetaCoq.Template.Universes]
UContext.dest [in MetaCoq.Template.Universes]
UContext.empty [in MetaCoq.Template.Universes]
UContext.instance [in MetaCoq.Template.Universes]
UContext.make [in MetaCoq.Template.Universes]
UContext.make' [in MetaCoq.Template.Universes]
UContext.t [in MetaCoq.Template.Universes]
uctx_of_udecl [in MetaCoq.Template.common.uGraph]
uctx_invariants [in MetaCoq.Template.common.uGraph]
uint_wB [in MetaCoq.Template.BasicAst]
uint_size [in MetaCoq.Template.BasicAst]
uint63_model [in MetaCoq.Template.BasicAst]
uint63_to_model [in MetaCoq.PCUIC.TemplateToPCUIC]
uint63_from_model [in MetaCoq.PCUIC.PCUICToTemplate]
UIP [in MetaCoq.Translations.times_bool_fun]
UIP [in MetaCoq.Translations.param_generous_packed]
unfold [in MetaCoq.Template.utils.MCList]
unfold_cofix [in MetaCoq.Template.Typing]
unfold_fix [in MetaCoq.Template.Typing]
unfold_cofix [in MetaCoq.PCUIC.Syntax.PCUICCases]
unfold_fix [in MetaCoq.PCUIC.Syntax.PCUICCases]
unfold_one_proj [in MetaCoq.SafeChecker.PCUICSafeConversion]
unfold_one_case [in MetaCoq.SafeChecker.PCUICSafeConversion]
unfold_constants [in MetaCoq.SafeChecker.PCUICSafeConversion]
unfold_one_fix [in MetaCoq.SafeChecker.PCUICSafeConversion]
unfold_one_case [in MetaCoq.Template.Checker]
unfold_one_fix [in MetaCoq.Template.Checker]
unfold_cofix [in MetaCoq.Erasure.EGlobalEnv]
unfold_fix [in MetaCoq.Erasure.EGlobalEnv]
univ [in MetaCoq.Examples.typing_correctness]
univ [in MetaCoq.Examples.metacoq_tour_prelude]
UnivConstraint.compare [in MetaCoq.Template.Universes]
UnivConstraint.eq [in MetaCoq.Template.Universes]
UnivConstraint.eq_leibniz [in MetaCoq.Template.Universes]
UnivConstraint.eq_equiv [in MetaCoq.Template.Universes]
UnivConstraint.lt [in MetaCoq.Template.Universes]
UnivConstraint.make [in MetaCoq.Template.Universes]
UnivConstraint.t [in MetaCoq.Template.Universes]
universes_entry_of_decl [in MetaCoq.Template.Universes]
universes_graph [in MetaCoq.Template.common.uGraph]
Universe.add_list_to_exprs [in MetaCoq.Template.Universes]
Universe.add_to_exprs [in MetaCoq.Template.Universes]
Universe.eqb [in MetaCoq.Template.Universes]
Universe.from_kernel_repr [in MetaCoq.Template.Universes]
Universe.get_is_level [in MetaCoq.Template.Universes]
Universe.get_univ_exprs [in MetaCoq.Template.Universes]
Universe.is_type_sort [in MetaCoq.Template.Universes]
Universe.is_prop [in MetaCoq.Template.Universes]
Universe.is_sprop [in MetaCoq.Template.Universes]
Universe.is_level [in MetaCoq.Template.Universes]
Universe.is_levels [in MetaCoq.Template.Universes]
Universe.make [in MetaCoq.Template.Universes]
Universe.of_levels [in MetaCoq.Template.Universes]
Universe.of_expr [in MetaCoq.Template.Universes]
Universe.on_sort [in MetaCoq.Template.Universes]
Universe.sort_of_product [in MetaCoq.Template.Universes]
Universe.sup [in MetaCoq.Template.Universes]
Universe.super [in MetaCoq.Template.Universes]
Universe.t [in MetaCoq.Template.Universes]
Universe.to_cuniv [in MetaCoq.Template.Universes]
Universe.type0 [in MetaCoq.Template.Universes]
Universe.type1 [in MetaCoq.Template.Universes]
unlift [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
unlift_renaming [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
unlift_opt_pred [in MetaCoq.Template.Typing]
unlift_opt_pred [in MetaCoq.PCUIC.PCUICTyping]
Unnamed_thm0 [in MetaCoq.Examples.constructor_tac]
Unnamed_thm [in MetaCoq.Examples.constructor_tac]
Unnamed_thm [in MetaCoq.Translations.times_bool_fun2]
Unnamed_thm [in MetaCoq.Translations.param_generous_packed]
unpack_sigma [in MetaCoq.Translations.MiniHoTT]
unpack_sigma [in MetaCoq.Translations.MiniHoTT_paths]
up [in MetaCoq.Template.EtaExpand]
Up [in MetaCoq.PCUIC.PCUICSigmaCalculus]
up [in MetaCoq.PCUIC.PCUICSigmaCalculus]
up [in MetaCoq.Erasure.ELiftSubst]
up [in MetaCoq.Template.LiftSubst]
Upn [in MetaCoq.PCUIC.PCUICSigmaCalculus]
upto_names [in MetaCoq.PCUIC.PCUICEquality]
urenaming [in MetaCoq.PCUIC.Syntax.PCUICRenameDef]
usubst [in MetaCoq.PCUIC.Syntax.PCUICInstDef]



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)