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)

P

PackKeyedPred [constructor, in Ssreflect.ssrbool]
PackKeyedQualifier [constructor, in Ssreflect.ssrbool]
pack_subCountType [definition, in Ssreflect.choice]
pack_subFinType [definition, in Ssreflect.fintype]
pairmap [definition, in Ssreflect.seq]
pairmapK [lemma, in Ssreflect.seq]
pairmap_cat [lemma, in Ssreflect.seq]
pair_of_tagK [lemma, in Ssreflect.choice]
pair_of_tag [definition, in Ssreflect.choice]
pair_of_and [definition, in Ssreflect.ssrfun]
pair_eq2 [lemma, in Ssreflect.eqtype]
pair_eq1 [lemma, in Ssreflect.eqtype]
pair_eqE [lemma, in Ssreflect.eqtype]
pair_eqP [lemma, in Ssreflect.eqtype]
pair_eq [definition, in Ssreflect.eqtype]
pair_andP [lemma, in Ssreflect.ssrbool]
pcancel [definition, in Ssreflect.ssrfun]
PcanChoiceMixin [lemma, in Ssreflect.choice]
PcanCountMixin [definition, in Ssreflect.choice]
PcanEqMixin [definition, in Ssreflect.eqtype]
PcanFinMixin [definition, in Ssreflect.fintype]
pcan_pickleK [lemma, in Ssreflect.choice]
pcan_pcomp [lemma, in Ssreflect.ssrfun]
pcan_inj [lemma, in Ssreflect.ssrfun]
pcan_enumP [lemma, in Ssreflect.fintype]
pcomp [definition, in Ssreflect.ssrfun]
PermSeq [section, in Ssreflect.seq]
PermSeq.T [variable, in Ssreflect.seq]
perm_undup_count [lemma, in Ssreflect.seq]
perm_eq_iotaP [lemma, in Ssreflect.seq]
perm_map [lemma, in Ssreflect.seq]
perm_to_subseq [lemma, in Ssreflect.seq]
perm_to_rem [lemma, in Ssreflect.seq]
perm_eqr [abbreviation, in Ssreflect.seq]
perm_eql [abbreviation, in Ssreflect.seq]
perm_eq_uniq [lemma, in Ssreflect.seq]
perm_uniq [lemma, in Ssreflect.seq]
perm_eq_small [lemma, in Ssreflect.seq]
perm_eq_size [lemma, in Ssreflect.seq]
perm_eq_mem [lemma, in Ssreflect.seq]
perm_filterC [lemma, in Ssreflect.seq]
perm_rotr [lemma, in Ssreflect.seq]
perm_rot [lemma, in Ssreflect.seq]
perm_rcons [lemma, in Ssreflect.seq]
perm_catCA [lemma, in Ssreflect.seq]
perm_catAC [lemma, in Ssreflect.seq]
perm_cat2r [lemma, in Ssreflect.seq]
perm_cons [lemma, in Ssreflect.seq]
perm_cat2l [lemma, in Ssreflect.seq]
perm_catC [lemma, in Ssreflect.seq]
perm_eqrP [lemma, in Ssreflect.seq]
perm_eqlP [lemma, in Ssreflect.seq]
perm_eqlE [lemma, in Ssreflect.seq]
perm_eqr [abbreviation, in Ssreflect.seq]
perm_eql [abbreviation, in Ssreflect.seq]
perm_eq_trans [lemma, in Ssreflect.seq]
perm_eq_sym [lemma, in Ssreflect.seq]
perm_eq_refl [lemma, in Ssreflect.seq]
perm_eqP [lemma, in Ssreflect.seq]
perm_eq [definition, in Ssreflect.seq]
ph [abbreviation, in Ssreflect.ssrbool]
ph [abbreviation, in Ssreflect.ssrbool]
Phant [constructor, in Ssreflect.ssreflect]
phant [inductive, in Ssreflect.ssreflect]
Phantom [constructor, in Ssreflect.ssreflect]
phantom [inductive, in Ssreflect.ssreflect]
phant_id [definition, in Ssreflect.ssrfun]
Pick [constructor, in Ssreflect.fintype]
pick [definition, in Ssreflect.fintype]
pickle [definition, in Ssreflect.choice]
pickleK [lemma, in Ssreflect.choice]
pickleK_inv [lemma, in Ssreflect.choice]
pickle_taggedK [lemma, in Ssreflect.choice]
pickle_tagged [definition, in Ssreflect.choice]
pickle_seqK [lemma, in Ssreflect.choice]
pickle_seq [definition, in Ssreflect.choice]
pickle_invK [lemma, in Ssreflect.choice]
pickle_inv [definition, in Ssreflect.choice]
pickP [lemma, in Ssreflect.fintype]
pick_spec [inductive, in Ssreflect.fintype]
pick_true [definition, in Ssreflect.fintype]
plusE [lemma, in Ssreflect.ssrnat]
pmap [definition, in Ssreflect.seq]
Pmap [section, in Ssreflect.seq]
PmapSub [section, in Ssreflect.seq]
PmapSub.p [variable, in Ssreflect.seq]
PmapSub.sT [variable, in Ssreflect.seq]
PmapSub.T [variable, in Ssreflect.seq]
pmapS_filter [lemma, in Ssreflect.seq]
pmap_sub_uniq [lemma, in Ssreflect.seq]
pmap_uniq [lemma, in Ssreflect.seq]
pmap_filter [lemma, in Ssreflect.seq]
Pmap.aT [variable, in Ssreflect.seq]
Pmap.f [variable, in Ssreflect.seq]
Pmap.fK [variable, in Ssreflect.seq]
Pmap.g [variable, in Ssreflect.seq]
Pmap.rT [variable, in Ssreflect.seq]
pop_succn [definition, in Ssreflect.ssrnat]
PosNotEq0 [constructor, in Ssreflect.ssrnat]
posnP [lemma, in Ssreflect.ssrnat]
pos_of_nat [definition, in Ssreflect.ssrnat]
pred [definition, in Ssreflect.ssrbool]
predArgType [definition, in Ssreflect.ssrbool]
predC [definition, in Ssreflect.ssrbool]
predC1 [definition, in Ssreflect.eqtype]
predD [definition, in Ssreflect.ssrbool]
predD1 [definition, in Ssreflect.eqtype]
predD1P [lemma, in Ssreflect.eqtype]
predI [definition, in Ssreflect.ssrbool]
Predicates [section, in Ssreflect.ssrbool]
Predicates.T [variable, in Ssreflect.ssrbool]
predn [abbreviation, in Ssreflect.ssrnat]
prednK [lemma, in Ssreflect.ssrnat]
predPredType [definition, in Ssreflect.ssrbool]
predT [definition, in Ssreflect.ssrbool]
predType [record, in Ssreflect.ssrbool]
PredType [constructor, in Ssreflect.ssrbool]
predT_subset [lemma, in Ssreflect.fintype]
predU [definition, in Ssreflect.ssrbool]
predU1 [definition, in Ssreflect.eqtype]
predU1l [lemma, in Ssreflect.eqtype]
predU1P [lemma, in Ssreflect.eqtype]
predU1r [lemma, in Ssreflect.eqtype]
predX [definition, in Ssreflect.eqtype]
predX_prod_enum [lemma, in Ssreflect.fintype]
pred_of_eq_seq [definition, in Ssreflect.seq]
pred_key [inductive, in Ssreflect.ssrbool]
pred_of_mem_pred [definition, in Ssreflect.ssrbool]
pred_of_argType [definition, in Ssreflect.ssrbool]
pred_class [abbreviation, in Ssreflect.ssrbool]
pred_of_mem [definition, in Ssreflect.ssrbool]
pred_sort [projection, in Ssreflect.ssrbool]
pred_of_simpl [definition, in Ssreflect.ssrbool]
pred0 [definition, in Ssreflect.ssrbool]
pred0b [definition, in Ssreflect.fintype]
pred0P [lemma, in Ssreflect.fintype]
pred0Pn [lemma, in Ssreflect.fintype]
pred1 [definition, in Ssreflect.eqtype]
pred1E [lemma, in Ssreflect.eqtype]
pred2 [definition, in Ssreflect.eqtype]
pred2P [lemma, in Ssreflect.eqtype]
pred3 [definition, in Ssreflect.eqtype]
pred4 [definition, in Ssreflect.eqtype]
prefix_subseq [lemma, in Ssreflect.seq]
preim [definition, in Ssreflect.ssrbool]
preim_seq [definition, in Ssreflect.fintype]
preim_iinv [lemma, in Ssreflect.fintype]
pre_image [lemma, in Ssreflect.fintype]
pre_symmetric [definition, in Ssreflect.ssrbool]
ProdEqType [section, in Ssreflect.eqtype]
ProdEqType.T1 [variable, in Ssreflect.eqtype]
ProdEqType.T2 [variable, in Ssreflect.eqtype]
ProdFinType [section, in Ssreflect.fintype]
ProdFinType.T1 [variable, in Ssreflect.fintype]
ProdFinType.T2 [variable, in Ssreflect.fintype]
prod_countType [definition, in Ssreflect.choice]
prod_countMixin [definition, in Ssreflect.choice]
prod_choiceType [definition, in Ssreflect.choice]
prod_choiceMixin [definition, in Ssreflect.choice]
prod_eqType [definition, in Ssreflect.eqtype]
prod_eqMixin [definition, in Ssreflect.eqtype]
prod_finType [definition, in Ssreflect.fintype]
prod_finMixin [definition, in Ssreflect.fintype]
prod_enumP [lemma, in Ssreflect.fintype]
prod_enum [definition, in Ssreflect.fintype]
proper [definition, in Ssreflect.fintype]
properE [lemma, in Ssreflect.fintype]
properP [lemma, in Ssreflect.fintype]
properxx [lemma, in Ssreflect.fintype]
proper_irrefl [lemma, in Ssreflect.fintype]
proper_card [lemma, in Ssreflect.fintype]
proper_sub_trans [lemma, in Ssreflect.fintype]
proper_trans [lemma, in Ssreflect.fintype]
proper_subn [lemma, in Ssreflect.fintype]
proper_sub [lemma, in Ssreflect.fintype]
prop_on2 [definition, in Ssreflect.ssrbool]
prop_on1 [definition, in Ssreflect.ssrbool]
prop_in3 [definition, in Ssreflect.ssrbool]
prop_in21 [definition, in Ssreflect.ssrbool]
prop_in12 [definition, in Ssreflect.ssrbool]
prop_in111 [definition, in Ssreflect.ssrbool]
prop_in2 [definition, in Ssreflect.ssrbool]
prop_in11 [definition, in Ssreflect.ssrbool]
prop_in1 [definition, in Ssreflect.ssrbool]
prop_for [definition, in Ssreflect.ssrbool]
prop_congr [lemma, in Ssreflect.ssrbool]
protect_term [definition, in Ssreflect.ssreflect]



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)