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)

C

cancel [definition, in Ssreflect.ssrfun]
CanChoiceMixin [definition, in Ssreflect.choice]
CanCountMixin [definition, in Ssreflect.choice]
CanEqMixin [definition, in Ssreflect.eqtype]
CanFinMixin [definition, in Ssreflect.fintype]
canF_invF [lemma, in Ssreflect.fintype]
canF_eq [lemma, in Ssreflect.fintype]
canF_RL [lemma, in Ssreflect.fintype]
canF_LR [lemma, in Ssreflect.fintype]
canF_sym [lemma, in Ssreflect.fintype]
canLR [lemma, in Ssreflect.ssrfun]
canLR_on [lemma, in Ssreflect.ssrbool]
canLR_in [lemma, in Ssreflect.ssrbool]
canRL [lemma, in Ssreflect.ssrfun]
canRL_on [lemma, in Ssreflect.ssrbool]
canRL_in [lemma, in Ssreflect.ssrbool]
can_comp [lemma, in Ssreflect.ssrfun]
can_inj [lemma, in Ssreflect.ssrfun]
can_pcan [lemma, in Ssreflect.ssrfun]
can_in_eq [lemma, in Ssreflect.eqtype]
can_eq [lemma, in Ssreflect.eqtype]
can_mono_in [lemma, in Ssreflect.ssrbool]
can_mono [lemma, in Ssreflect.ssrbool]
can_in_inj [lemma, in Ssreflect.ssrbool]
can2_eq [lemma, in Ssreflect.eqtype]
can2_mem_pmap [lemma, in Ssreflect.seq]
cardC [lemma, in Ssreflect.fintype]
cardC1 [lemma, in Ssreflect.fintype]
CardDef [module, in Ssreflect.fintype]
CardDefSig [module, in Ssreflect.fintype]
CardDefSig.card [axiom, in Ssreflect.fintype]
CardDefSig.cardEdef [axiom, in Ssreflect.fintype]
CardDef.card [definition, in Ssreflect.fintype]
CardDef.cardEdef [definition, in Ssreflect.fintype]
cardD1 [lemma, in Ssreflect.fintype]
cardE [lemma, in Ssreflect.fintype]
CardFunImage [section, in Ssreflect.fintype]
CardFunImage.card_range [variable, in Ssreflect.fintype]
CardFunImage.f [variable, in Ssreflect.fintype]
CardFunImage.injf [variable, in Ssreflect.fintype]
CardFunImage.T [variable, in Ssreflect.fintype]
CardFunImage.T' [variable, in Ssreflect.fintype]
cardID [lemma, in Ssreflect.fintype]
CardSig [section, in Ssreflect.fintype]
CardSig.P [variable, in Ssreflect.fintype]
CardSig.T [variable, in Ssreflect.fintype]
cardT [lemma, in Ssreflect.fintype]
cardUI [lemma, in Ssreflect.fintype]
cardU1 [lemma, in Ssreflect.fintype]
cardX [lemma, in Ssreflect.fintype]
card_sum [lemma, in Ssreflect.fintype]
card_tagged [lemma, in Ssreflect.fintype]
card_prod [lemma, in Ssreflect.fintype]
card_ord [lemma, in Ssreflect.fintype]
card_sig [lemma, in Ssreflect.fintype]
card_sub [lemma, in Ssreflect.fintype]
card_option [lemma, in Ssreflect.fintype]
card_bool [lemma, in Ssreflect.fintype]
card_unit [lemma, in Ssreflect.fintype]
card_seq_sub [lemma, in Ssreflect.fintype]
card_preim [lemma, in Ssreflect.fintype]
card_codom [lemma, in Ssreflect.fintype]
card_image [lemma, in Ssreflect.fintype]
card_in_image [lemma, in Ssreflect.fintype]
card_gt0P [lemma, in Ssreflect.fintype]
card_uniqP [lemma, in Ssreflect.fintype]
card_size [lemma, in Ssreflect.fintype]
card_unlock [definition, in Ssreflect.fintype]
card_def [abbreviation, in Ssreflect.fintype]
card_type [abbreviation, in Ssreflect.fintype]
card0 [lemma, in Ssreflect.fintype]
card0_eq [lemma, in Ssreflect.fintype]
card1 [lemma, in Ssreflect.fintype]
card2 [lemma, in Ssreflect.fintype]
cast_ord_inj [lemma, in Ssreflect.fintype]
cast_ordKV [lemma, in Ssreflect.fintype]
cast_ordK [lemma, in Ssreflect.fintype]
cast_ord_comp [lemma, in Ssreflect.fintype]
cast_ord_id [lemma, in Ssreflect.fintype]
cast_ord [definition, in Ssreflect.fintype]
cast_ord_proof [lemma, in Ssreflect.fintype]
cat [definition, in Ssreflect.seq]
catA [lemma, in Ssreflect.seq]
catCA_perm_subst [lemma, in Ssreflect.seq]
catCA_perm_ind [lemma, in Ssreflect.seq]
catcomp [definition, in Ssreflect.ssrfun]
catrev [definition, in Ssreflect.seq]
catrevE [lemma, in Ssreflect.seq]
catrev_catr [lemma, in Ssreflect.seq]
catrev_catl [lemma, in Ssreflect.seq]
cats0 [lemma, in Ssreflect.seq]
cats1 [lemma, in Ssreflect.seq]
cat_subseq [lemma, in Ssreflect.seq]
cat_uniq [lemma, in Ssreflect.seq]
cat_take_drop [lemma, in Ssreflect.seq]
cat_rcons [lemma, in Ssreflect.seq]
cat_nseq [lemma, in Ssreflect.seq]
cat_cons [lemma, in Ssreflect.seq]
cat0s [lemma, in Ssreflect.seq]
cat1s [lemma, in Ssreflect.seq]
check_applicative_mem_pred [definition, in Ssreflect.ssrbool]
Choice [module, in Ssreflect.choice]
choice [library]
ChoiceTheory [section, in Ssreflect.choice]
ChoiceTheory.OneType [section, in Ssreflect.choice]
ChoiceTheory.OneType.CanChoice [section, in Ssreflect.choice]
ChoiceTheory.OneType.CanChoice.f [variable, in Ssreflect.choice]
ChoiceTheory.OneType.CanChoice.sT [variable, in Ssreflect.choice]
ChoiceTheory.OneType.SubChoice [section, in Ssreflect.choice]
ChoiceTheory.OneType.SubChoice.P [variable, in Ssreflect.choice]
ChoiceTheory.OneType.SubChoice.sT [variable, in Ssreflect.choice]
ChoiceTheory.OneType.T [variable, in Ssreflect.choice]
ChoiceTheory.TagChoice [section, in Ssreflect.choice]
ChoiceTheory.TagChoice.I [variable, in Ssreflect.choice]
ChoiceTheory.TagChoice.T_ [variable, in Ssreflect.choice]
Choice.base [projection, in Ssreflect.choice]
Choice.class [definition, in Ssreflect.choice]
Choice.Class [constructor, in Ssreflect.choice]
Choice.ClassDef [section, in Ssreflect.choice]
Choice.ClassDef.cT [variable, in Ssreflect.choice]
Choice.ClassDef.T [variable, in Ssreflect.choice]
Choice.ClassDef.xT [variable, in Ssreflect.choice]
Choice.class_of [record, in Ssreflect.choice]
Choice.clone [definition, in Ssreflect.choice]
Choice.eqType [definition, in Ssreflect.choice]
Choice.Exports [module, in Ssreflect.choice]
Choice.Exports.choiceMixin [abbreviation, in Ssreflect.choice]
Choice.Exports.ChoiceType [abbreviation, in Ssreflect.choice]
Choice.Exports.choiceType [abbreviation, in Ssreflect.choice]
[ choiceType of _ ] (form_scope) [notation, in Ssreflect.choice]
[ choiceType of _ for _ ] (form_scope) [notation, in Ssreflect.choice]
Choice.find [projection, in Ssreflect.choice]
Choice.InternalTheory [module, in Ssreflect.choice]
Choice.InternalTheory.complete [lemma, in Ssreflect.choice]
Choice.InternalTheory.correct [lemma, in Ssreflect.choice]
Choice.InternalTheory.extensional [lemma, in Ssreflect.choice]
Choice.InternalTheory.find [definition, in Ssreflect.choice]
Choice.InternalTheory.InternalTheory [section, in Ssreflect.choice]
Choice.InternalTheory.InternalTheory.T [variable, in Ssreflect.choice]
Choice.InternalTheory.xchoose_subproof [lemma, in Ssreflect.choice]
Choice.mixin [projection, in Ssreflect.choice]
Choice.Mixin [constructor, in Ssreflect.choice]
Choice.mixin_of [record, in Ssreflect.choice]
Choice.pack [definition, in Ssreflect.choice]
Choice.Pack [constructor, in Ssreflect.choice]
Choice.sort [projection, in Ssreflect.choice]
Choice.type [record, in Ssreflect.choice]
Choice.xclass [abbreviation, in Ssreflect.choice]
choose [definition, in Ssreflect.choice]
chooseP [lemma, in Ssreflect.choice]
choose_id [lemma, in Ssreflect.choice]
classically [definition, in Ssreflect.ssrbool]
classicP [lemma, in Ssreflect.ssrbool]
classic_pick [lemma, in Ssreflect.ssrbool]
classic_imply [lemma, in Ssreflect.ssrbool]
classic_EM [lemma, in Ssreflect.ssrbool]
classic_bind [lemma, in Ssreflect.ssrbool]
clone_subType [definition, in Ssreflect.eqtype]
clone_pred [definition, in Ssreflect.ssrbool]
CodeSeq [module, in Ssreflect.choice]
CodeSeq.code [definition, in Ssreflect.choice]
CodeSeq.codeK [lemma, in Ssreflect.choice]
CodeSeq.decode [definition, in Ssreflect.choice]
CodeSeq.decodeK [lemma, in Ssreflect.choice]
CodeSeq.decode_rec [definition, in Ssreflect.choice]
CodeSeq.gtn_decode [lemma, in Ssreflect.choice]
CodeSeq.ltn_code [lemma, in Ssreflect.choice]
[ rec _ , _ , _ ] [notation, in Ssreflect.choice]
codom [definition, in Ssreflect.fintype]
codomE [lemma, in Ssreflect.fintype]
codomP [lemma, in Ssreflect.fintype]
codom_val [lemma, in Ssreflect.fintype]
codom_f [lemma, in Ssreflect.fintype]
coerced_frel [abbreviation, in Ssreflect.eqtype]
collective_pred_of_simpl [definition, in Ssreflect.ssrbool]
collective_pred [definition, in Ssreflect.ssrbool]
commutative [definition, in Ssreflect.ssrfun]
comp [abbreviation, in Ssreflect.ssrfun]
comp [abbreviation, in Ssreflect.ssrfun]
comparable [definition, in Ssreflect.eqtype]
comparableClass [definition, in Ssreflect.eqtype]
ComparableType [section, in Ssreflect.eqtype]
ComparableType.Hcompare [variable, in Ssreflect.eqtype]
ComparableType.T [variable, in Ssreflect.eqtype]
compareb [definition, in Ssreflect.eqtype]
CompareNatEq [constructor, in Ssreflect.ssrnat]
CompareNatGt [constructor, in Ssreflect.ssrnat]
CompareNatLt [constructor, in Ssreflect.ssrnat]
compareP [lemma, in Ssreflect.eqtype]
compare_nat [inductive, in Ssreflect.ssrnat]
Composition [section, in Ssreflect.ssrfun]
Composition.A [variable, in Ssreflect.ssrfun]
Composition.B [variable, in Ssreflect.ssrfun]
Composition.C [variable, in Ssreflect.ssrfun]
congr1 [definition, in Ssreflect.ssrfun]
congr2 [definition, in Ssreflect.ssrfun]
Cons [abbreviation, in Ssreflect.seq]
constant [definition, in Ssreflect.seq]
constantP [lemma, in Ssreflect.seq]
constant_nseq [lemma, in Ssreflect.seq]
cons_uniq [lemma, in Ssreflect.seq]
contra [lemma, in Ssreflect.ssrbool]
contraFeq [lemma, in Ssreflect.eqtype]
contraFF [lemma, in Ssreflect.ssrbool]
contraFN [lemma, in Ssreflect.ssrbool]
contraFneq [lemma, in Ssreflect.eqtype]
contraFT [lemma, in Ssreflect.ssrbool]
contraL [lemma, in Ssreflect.ssrbool]
contraLR [lemma, in Ssreflect.ssrbool]
contraNeq [lemma, in Ssreflect.eqtype]
contraNF [lemma, in Ssreflect.ssrbool]
contraNN [definition, in Ssreflect.ssrbool]
contraNneq [lemma, in Ssreflect.eqtype]
contraNT [definition, in Ssreflect.ssrbool]
Contrapositives [section, in Ssreflect.eqtype]
Contrapositives.T [variable, in Ssreflect.eqtype]
contraR [lemma, in Ssreflect.ssrbool]
contraT [lemma, in Ssreflect.ssrbool]
contraTeq [lemma, in Ssreflect.eqtype]
contraTF [lemma, in Ssreflect.ssrbool]
contraTN [definition, in Ssreflect.ssrbool]
contraTneq [lemma, in Ssreflect.eqtype]
contraTT [definition, in Ssreflect.ssrbool]
contra_neq [lemma, in Ssreflect.eqtype]
contra_eq [lemma, in Ssreflect.eqtype]
contra_eqT [lemma, in Ssreflect.eqtype]
contra_eqF [lemma, in Ssreflect.eqtype]
contra_eqN [lemma, in Ssreflect.eqtype]
count [definition, in Ssreflect.seq]
Countable [module, in Ssreflect.choice]
CountableDataTypes [section, in Ssreflect.choice]
CountableTheory [section, in Ssreflect.choice]
CountableTheory.T [variable, in Ssreflect.choice]
Countable.base [projection, in Ssreflect.choice]
Countable.ChoiceMixin [definition, in Ssreflect.choice]
Countable.choiceType [definition, in Ssreflect.choice]
Countable.class [definition, in Ssreflect.choice]
Countable.Class [constructor, in Ssreflect.choice]
Countable.ClassDef [section, in Ssreflect.choice]
Countable.ClassDef.cT [variable, in Ssreflect.choice]
Countable.ClassDef.T [variable, in Ssreflect.choice]
Countable.ClassDef.xT [variable, in Ssreflect.choice]
Countable.class_of [record, in Ssreflect.choice]
Countable.clone [definition, in Ssreflect.choice]
Countable.EqMixin [definition, in Ssreflect.choice]
Countable.eqType [definition, in Ssreflect.choice]
Countable.Exports [module, in Ssreflect.choice]
Countable.Exports.CountChoiceMixin [abbreviation, in Ssreflect.choice]
Countable.Exports.CountMixin [abbreviation, in Ssreflect.choice]
Countable.Exports.CountType [abbreviation, in Ssreflect.choice]
Countable.Exports.countType [abbreviation, in Ssreflect.choice]
[ countType of _ ] (form_scope) [notation, in Ssreflect.choice]
[ countType of _ for _ ] (form_scope) [notation, in Ssreflect.choice]
Countable.mixin [projection, in Ssreflect.choice]
Countable.Mixin [constructor, in Ssreflect.choice]
Countable.mixin_of [record, in Ssreflect.choice]
Countable.pack [definition, in Ssreflect.choice]
Countable.Pack [constructor, in Ssreflect.choice]
Countable.pickle [projection, in Ssreflect.choice]
Countable.pickleK [projection, in Ssreflect.choice]
Countable.sort [projection, in Ssreflect.choice]
Countable.type [record, in Ssreflect.choice]
Countable.unpickle [projection, in Ssreflect.choice]
Countable.xclass [abbreviation, in Ssreflect.choice]
count_map [lemma, in Ssreflect.seq]
count_mem_uniq [lemma, in Ssreflect.seq]
count_uniq_mem [lemma, in Ssreflect.seq]
count_memPn [lemma, in Ssreflect.seq]
count_rev [lemma, in Ssreflect.seq]
count_mem [abbreviation, in Ssreflect.seq]
count_filter [lemma, in Ssreflect.seq]
count_predC [lemma, in Ssreflect.seq]
count_predUI [lemma, in Ssreflect.seq]
count_predT [lemma, in Ssreflect.seq]
count_pred0 [lemma, in Ssreflect.seq]
count_cat [lemma, in Ssreflect.seq]
count_size [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)