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 (3098 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 (294 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 (28 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 (397 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 (9 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 (1414 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 (80 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 (7 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 (35 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 (35 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 (135 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 (84 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 (555 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 (25 entries)

D

dc [abbreviation, in Ssreflect.choice]
decidable [definition, in Ssreflect.ssrbool]
decP [definition, in Ssreflect.ssrbool]
decPcases [lemma, in Ssreflect.ssrbool]
DefaultKeying [module, in Ssreflect.ssrbool]
DefaultKeying.default_keyed_qualifier [definition, in Ssreflect.ssrbool]
DefaultKeying.default_keyed_pred [definition, in Ssreflect.ssrbool]
DefaultPredKey [constructor, in Ssreflect.ssrbool]
dependentReturnType [definition, in Ssreflect.ssreflect]
dinjectiveb [definition, in Ssreflect.fintype]
dinjectiveP [lemma, in Ssreflect.fintype]
dinjectivePn [lemma, in Ssreflect.fintype]
disjoint [definition, in Ssreflect.fintype]
disjointU [lemma, in Ssreflect.fintype]
disjointU1 [lemma, in Ssreflect.fintype]
disjoint_cat [lemma, in Ssreflect.fintype]
disjoint_has [lemma, in Ssreflect.fintype]
disjoint_cons [lemma, in Ssreflect.fintype]
disjoint_trans [lemma, in Ssreflect.fintype]
disjoint_subset [lemma, in Ssreflect.fintype]
disjoint_sym [lemma, in Ssreflect.fintype]
disjoint0 [lemma, in Ssreflect.fintype]
disjoint1 [lemma, in Ssreflect.fintype]
double [definition, in Ssreflect.ssrnat]
doubleB [lemma, in Ssreflect.ssrnat]
doubleD [lemma, in Ssreflect.ssrnat]
doubleE [lemma, in Ssreflect.ssrnat]
doubleK [lemma, in Ssreflect.ssrnat]
doubleMl [lemma, in Ssreflect.ssrnat]
doubleMr [lemma, in Ssreflect.ssrnat]
doubleS [lemma, in Ssreflect.ssrnat]
double_inj [definition, in Ssreflect.ssrnat]
double_eq0 [lemma, in Ssreflect.ssrnat]
double_gt0 [lemma, in Ssreflect.ssrnat]
double_rec [definition, in Ssreflect.ssrnat]
double0 [lemma, in Ssreflect.ssrnat]
drop [definition, in Ssreflect.seq]
drop_nth [lemma, in Ssreflect.seq]
drop_rcons [lemma, in Ssreflect.seq]
drop_size_cat [lemma, in Ssreflect.seq]
drop_cat [lemma, in Ssreflect.seq]
drop_cons [lemma, in Ssreflect.seq]
drop_size [lemma, in Ssreflect.seq]
drop_oversize [lemma, in Ssreflect.seq]
drop_behead [lemma, in Ssreflect.seq]
drop0 [lemma, in Ssreflect.seq]
drop1 [lemma, in Ssreflect.seq]



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 (3098 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 (294 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 (28 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 (397 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 (9 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 (1414 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 (80 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 (7 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 (35 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 (35 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 (135 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 (84 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 (555 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 (25 entries)