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 (19204 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 (228 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 (298 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 (1273 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 (313 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 (8163 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 (1514 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 (52 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 (352 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 (534 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 (727 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 (402 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 (333 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 (4833 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 (182 entries)

J

joinable [definition, in MetaRocq.PCUIC.PCUICConfluence]
joinable_proper [instance, in MetaRocq.PCUIC.PCUICConfluence]
judgment_cons [constructor, in MetaRocq.PCUIC.Bidirectional.BDTyping]
judgment_map [definition, in MetaRocq.Common.BasicAst]
judgment_ [record, in MetaRocq.Common.BasicAst]
j_decl_s [abbreviation, in MetaRocq.Common.BasicAst]
j_decl [abbreviation, in MetaRocq.Common.BasicAst]
j_vdef [abbreviation, in MetaRocq.Common.BasicAst]
j_vass_s [abbreviation, in MetaRocq.Common.BasicAst]
j_vass [abbreviation, in MetaRocq.Common.BasicAst]
j_univ [projection, in MetaRocq.Common.BasicAst]
j_typ [projection, in MetaRocq.Common.BasicAst]
j_term [projection, in MetaRocq.Common.BasicAst]