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)

S

sameP [lemma, in Ssreflect.ssrbool]
Scan [section, in Ssreflect.seq]
scanl [definition, in Ssreflect.seq]
scanlK [lemma, in Ssreflect.seq]
scanl_cat [lemma, in Ssreflect.seq]
Scan.f [variable, in Ssreflect.seq]
Scan.g [variable, in Ssreflect.seq]
Scan.T1 [variable, in Ssreflect.seq]
Scan.T2 [variable, in Ssreflect.seq]
Scan.x1 [variable, in Ssreflect.seq]
Scan.x2 [variable, in Ssreflect.seq]
self_inverse [definition, in Ssreflect.ssrfun]
seq [abbreviation, in Ssreflect.seq]
seq [library]
SeqFinType [section, in Ssreflect.fintype]
SeqFinType.s [variable, in Ssreflect.fintype]
SeqFinType.T [variable, in Ssreflect.fintype]
seqn [definition, in Ssreflect.seq]
seqn_rec [definition, in Ssreflect.seq]
seqn_type [definition, in Ssreflect.seq]
SeqSub [constructor, in Ssreflect.fintype]
Sequences [section, in Ssreflect.seq]
Sequences.n0 [variable, in Ssreflect.seq]
Sequences.SeqFind [section, in Ssreflect.seq]
Sequences.SeqFind.a [variable, in Ssreflect.seq]
Sequences.SubPred [section, in Ssreflect.seq]
Sequences.SubPred.a1 [variable, in Ssreflect.seq]
Sequences.SubPred.a2 [variable, in Ssreflect.seq]
Sequences.SubPred.s12 [variable, in Ssreflect.seq]
Sequences.T [variable, in Ssreflect.seq]
Sequences.x0 [variable, in Ssreflect.seq]
_ ++ _ (seq_scope) [notation, in Ssreflect.seq]
seq_countType [definition, in Ssreflect.choice]
seq_countMixin [definition, in Ssreflect.choice]
seq_choiceType [definition, in Ssreflect.choice]
seq_choiceMixin [lemma, in Ssreflect.choice]
seq_of_optK [lemma, in Ssreflect.choice]
seq_of_opt [definition, in Ssreflect.choice]
seq_predType [definition, in Ssreflect.seq]
seq_eqType [definition, in Ssreflect.seq]
seq_eqMixin [definition, in Ssreflect.seq]
seq_sub_subFinType [definition, in Ssreflect.fintype]
seq_sub_finType [definition, in Ssreflect.fintype]
seq_sub_finMixin [definition, in Ssreflect.fintype]
seq_sub_subCountType [definition, in Ssreflect.fintype]
seq_sub_countType [definition, in Ssreflect.fintype]
seq_sub_countMixin [definition, in Ssreflect.fintype]
seq_sub_pickleK [lemma, in Ssreflect.fintype]
seq_sub_unpickle [definition, in Ssreflect.fintype]
seq_sub_pickle [definition, in Ssreflect.fintype]
seq_sub_enum [definition, in Ssreflect.fintype]
seq_sub_choiceType [definition, in Ssreflect.fintype]
seq_sub_choiceMixin [definition, in Ssreflect.fintype]
seq_sub_eqType [definition, in Ssreflect.fintype]
seq_sub_eqMixin [definition, in Ssreflect.fintype]
seq_sub_subType [definition, in Ssreflect.fintype]
seq_sub [record, in Ssreflect.fintype]
seq2_ind [lemma, in Ssreflect.seq]
set_nth_default [lemma, in Ssreflect.seq]
set_set_nth [lemma, in Ssreflect.seq]
set_nth_nil [lemma, in Ssreflect.seq]
set_nth [definition, in Ssreflect.seq]
shape [definition, in Ssreflect.seq]
Sig [section, in Ssreflect.ssrfun]
SigEqType [section, in Ssreflect.eqtype]
SigEqType.P [variable, in Ssreflect.eqtype]
SigEqType.T [variable, in Ssreflect.eqtype]
SigProj [section, in Ssreflect.eqtype]
SigProj.P [variable, in Ssreflect.eqtype]
SigProj.Q [variable, in Ssreflect.eqtype]
SigProj.T [variable, in Ssreflect.eqtype]
sigW [lemma, in Ssreflect.choice]
sig_subCountType [definition, in Ssreflect.choice]
sig_countType [definition, in Ssreflect.choice]
sig_countMixin [definition, in Ssreflect.choice]
sig_choiceType [definition, in Ssreflect.choice]
sig_choiceMixin [definition, in Ssreflect.choice]
sig_eqW [lemma, in Ssreflect.choice]
sig_of_sig2 [definition, in Ssreflect.ssrfun]
sig_eqType [definition, in Ssreflect.eqtype]
sig_eqMixin [definition, in Ssreflect.eqtype]
sig_subType [definition, in Ssreflect.eqtype]
sig_subFinType [definition, in Ssreflect.fintype]
sig_finType [definition, in Ssreflect.fintype]
sig_finMixin [definition, in Ssreflect.fintype]
Sig.P [variable, in Ssreflect.ssrfun]
Sig.Q [variable, in Ssreflect.ssrfun]
Sig.T [variable, in Ssreflect.ssrfun]
sig2W [lemma, in Ssreflect.choice]
sig2_eqW [lemma, in Ssreflect.choice]
SimplFun [constructor, in Ssreflect.ssrfun]
SimplFun [section, in Ssreflect.ssrfun]
SimplFunDelta [definition, in Ssreflect.ssrfun]
SimplFun.aT [variable, in Ssreflect.ssrfun]
SimplFun.rT [variable, in Ssreflect.ssrfun]
SimplPred [definition, in Ssreflect.ssrbool]
simplPredType [definition, in Ssreflect.ssrbool]
SimplRel [definition, in Ssreflect.ssrbool]
simpl_fun [inductive, in Ssreflect.ssrfun]
simpl_predE [lemma, in Ssreflect.ssrbool]
simpl_mem.pT [variable, in Ssreflect.ssrbool]
simpl_mem.T [variable, in Ssreflect.ssrbool]
simpl_mem [section, in Ssreflect.ssrbool]
simpl_rel [definition, in Ssreflect.ssrbool]
simpl_pred [definition, in Ssreflect.ssrbool]
size [definition, in Ssreflect.seq]
size_allpairs [lemma, in Ssreflect.seq]
size_flatten [lemma, in Ssreflect.seq]
size_zip [lemma, in Ssreflect.seq]
size_scanl [lemma, in Ssreflect.seq]
size_pairmap [lemma, in Ssreflect.seq]
size_mkseq [lemma, in Ssreflect.seq]
size_iota [lemma, in Ssreflect.seq]
size_pmap_sub [lemma, in Ssreflect.seq]
size_pmap [lemma, in Ssreflect.seq]
size_map [lemma, in Ssreflect.seq]
size_rem [lemma, in Ssreflect.seq]
size_subseq_leqif [lemma, in Ssreflect.seq]
size_subseq [lemma, in Ssreflect.seq]
size_mask [lemma, in Ssreflect.seq]
size_rotr [lemma, in Ssreflect.seq]
size_incr_nth [lemma, in Ssreflect.seq]
size_undup [lemma, in Ssreflect.seq]
size_eq0 [lemma, in Ssreflect.seq]
size_rev [lemma, in Ssreflect.seq]
size_rot [lemma, in Ssreflect.seq]
size_take [lemma, in Ssreflect.seq]
size_takel [lemma, in Ssreflect.seq]
size_drop [lemma, in Ssreflect.seq]
size_filter [lemma, in Ssreflect.seq]
size_set_nth [lemma, in Ssreflect.seq]
size_belast [lemma, in Ssreflect.seq]
size_rcons [lemma, in Ssreflect.seq]
size_cat [lemma, in Ssreflect.seq]
size_nseq [lemma, in Ssreflect.seq]
size_ncons [lemma, in Ssreflect.seq]
size_behead [lemma, in Ssreflect.seq]
size_enum_ord [lemma, in Ssreflect.fintype]
size_codom [lemma, in Ssreflect.fintype]
size_image [lemma, in Ssreflect.fintype]
size0nil [lemma, in Ssreflect.seq]
size1_zip [lemma, in Ssreflect.seq]
size2_zip [lemma, in Ssreflect.seq]
some [abbreviation, in Ssreflect.ssrfun]
Some_inj [lemma, in Ssreflect.ssrfun]
sort_of_simpl_pred [definition, in Ssreflect.ssrbool]
split [definition, in Ssreflect.fintype]
SplitHi [constructor, in Ssreflect.fintype]
splitK [lemma, in Ssreflect.fintype]
SplitLo [constructor, in Ssreflect.fintype]
splitP [lemma, in Ssreflect.fintype]
split_spec [inductive, in Ssreflect.fintype]
split_subproof [lemma, in Ssreflect.fintype]
sqrnD [lemma, in Ssreflect.ssrnat]
sqrnD_sub [lemma, in Ssreflect.ssrnat]
sqrn_inj [lemma, in Ssreflect.ssrnat]
sqrn_gt0 [lemma, in Ssreflect.ssrnat]
sqrn_sub [lemma, in Ssreflect.ssrnat]
ssrbool [library]
ssreflect [library]
ssrfun [library]
ssrmatching [library]
SsrMatchingSyntax [module, in Ssreflect.ssrmatching]
SsrMatchingSyntax.LHS [abbreviation, in Ssreflect.ssrmatching]
SsrMatchingSyntax.RHS [abbreviation, in Ssreflect.ssrmatching]
( _ in _ ) (ssrpatternscope) [notation, in Ssreflect.ssrmatching]
ssrnat [library]
SsrSyntax [module, in Ssreflect.ssreflect]
ssr_congr_arrow [lemma, in Ssreflect.ssreflect]
ssr_wlog [definition, in Ssreflect.ssreflect]
ssr_suff [definition, in Ssreflect.ssreflect]
ssr_have_let [definition, in Ssreflect.ssreflect]
ssr_have [definition, in Ssreflect.ssreflect]
ssr_converse [definition, in Ssreflect.ssreflect]
ssval [projection, in Ssreflect.fintype]
ssvalP [projection, in Ssreflect.fintype]
Sub [projection, in Ssreflect.eqtype]
subCountType [record, in Ssreflect.choice]
SubCountType [constructor, in Ssreflect.choice]
SubCountType [section, in Ssreflect.choice]
SubCountType.P [variable, in Ssreflect.choice]
SubCountType.T [variable, in Ssreflect.choice]
subCount_sort [projection, in Ssreflect.choice]
SubEqMixin [definition, in Ssreflect.eqtype]
SubEqType [section, in Ssreflect.eqtype]
SubEqType.P [variable, in Ssreflect.eqtype]
SubEqType.sT [variable, in Ssreflect.eqtype]
SubEqType.T [variable, in Ssreflect.eqtype]
SubFinMixin [definition, in Ssreflect.fintype]
SubFinMixin_for [definition, in Ssreflect.fintype]
subFinType [record, in Ssreflect.fintype]
SubFinType [constructor, in Ssreflect.fintype]
SubFinType [section, in Ssreflect.fintype]
subFinType_finType [definition, in Ssreflect.fintype]
subFinType_subCountType [definition, in Ssreflect.fintype]
SubFinType.P [variable, in Ssreflect.fintype]
SubFinType.T [variable, in Ssreflect.fintype]
subFin_mixin [definition, in Ssreflect.fintype]
subFin_sort [projection, in Ssreflect.fintype]
SubK [lemma, in Ssreflect.eqtype]
subKn [lemma, in Ssreflect.ssrnat]
subn [definition, in Ssreflect.ssrnat]
subnAC [lemma, in Ssreflect.ssrnat]
subnBA [lemma, in Ssreflect.ssrnat]
subnDA [lemma, in Ssreflect.ssrnat]
subnDl [lemma, in Ssreflect.ssrnat]
subnDr [lemma, in Ssreflect.ssrnat]
subnE [lemma, in Ssreflect.ssrnat]
subnK [lemma, in Ssreflect.ssrnat]
subnKC [lemma, in Ssreflect.ssrnat]
subnn [lemma, in Ssreflect.ssrnat]
subnS [lemma, in Ssreflect.ssrnat]
subnSK [lemma, in Ssreflect.ssrnat]
subn_sqr [lemma, in Ssreflect.ssrnat]
subn_if_gt [lemma, in Ssreflect.ssrnat]
subn_eq0 [lemma, in Ssreflect.ssrnat]
subn_gt0 [lemma, in Ssreflect.ssrnat]
subn_rec [definition, in Ssreflect.ssrnat]
subn0 [lemma, in Ssreflect.ssrnat]
subn1 [lemma, in Ssreflect.ssrnat]
subn2 [lemma, in Ssreflect.ssrnat]
subon_bij [lemma, in Ssreflect.ssrbool]
subon1 [lemma, in Ssreflect.ssrbool]
subon1l [lemma, in Ssreflect.ssrbool]
subon2 [lemma, in Ssreflect.ssrbool]
SubP [lemma, in Ssreflect.eqtype]
subpred [definition, in Ssreflect.ssrbool]
subrel [definition, in Ssreflect.ssrbool]
subrelUl [lemma, in Ssreflect.ssrbool]
subrelUr [lemma, in Ssreflect.ssrbool]
subseq [definition, in Ssreflect.seq]
Subseq [section, in Ssreflect.seq]
subseqP [lemma, in Ssreflect.seq]
subseq_uniqP [lemma, in Ssreflect.seq]
subseq_filter [lemma, in Ssreflect.seq]
subseq_uniq [lemma, in Ssreflect.seq]
subseq_rcons [lemma, in Ssreflect.seq]
subseq_cons [lemma, in Ssreflect.seq]
subseq_refl [lemma, in Ssreflect.seq]
subseq_trans [lemma, in Ssreflect.seq]
Subseq.T [variable, in Ssreflect.seq]
subseq0 [lemma, in Ssreflect.seq]
SubsetDef [module, in Ssreflect.fintype]
SubsetDefSig [module, in Ssreflect.fintype]
SubsetDefSig.subset [axiom, in Ssreflect.fintype]
SubsetDefSig.subsetEdef [axiom, in Ssreflect.fintype]
SubsetDef.subset [definition, in Ssreflect.fintype]
SubsetDef.subsetEdef [definition, in Ssreflect.fintype]
subsetE [lemma, in Ssreflect.fintype]
subsetP [lemma, in Ssreflect.fintype]
subsetPn [lemma, in Ssreflect.fintype]
subset_disjoint [lemma, in Ssreflect.fintype]
subset_all [lemma, in Ssreflect.fintype]
subset_trans [lemma, in Ssreflect.fintype]
subset_leqif_card [lemma, in Ssreflect.fintype]
subset_cardP [lemma, in Ssreflect.fintype]
subset_eqP [lemma, in Ssreflect.fintype]
subset_pred1 [lemma, in Ssreflect.fintype]
subset_predT [lemma, in Ssreflect.fintype]
subset_leq_card [lemma, in Ssreflect.fintype]
subset_unlock [definition, in Ssreflect.fintype]
subset_def [abbreviation, in Ssreflect.fintype]
subset_type [abbreviation, in Ssreflect.fintype]
subSKn [lemma, in Ssreflect.ssrnat]
subSn [lemma, in Ssreflect.ssrnat]
subSnn [lemma, in Ssreflect.ssrnat]
SubSpec [constructor, in Ssreflect.eqtype]
subSS [lemma, in Ssreflect.ssrnat]
subType [record, in Ssreflect.eqtype]
SubType [constructor, in Ssreflect.eqtype]
SubType [section, in Ssreflect.eqtype]
SubType.P [variable, in Ssreflect.eqtype]
SubType.sT [variable, in Ssreflect.eqtype]
SubType.T [variable, in Ssreflect.eqtype]
subxx [lemma, in Ssreflect.fintype]
subxx_hint [lemma, in Ssreflect.fintype]
sub_countType [definition, in Ssreflect.choice]
sub_countMixin [definition, in Ssreflect.choice]
sub_choiceType [definition, in Ssreflect.choice]
sub_choiceClass [definition, in Ssreflect.choice]
sub_choiceMixin [definition, in Ssreflect.choice]
sub_eqType [definition, in Ssreflect.eqtype]
sub_eqMixin [definition, in Ssreflect.eqtype]
Sub_spec [inductive, in Ssreflect.eqtype]
sub_sort [projection, in Ssreflect.eqtype]
sub_all [lemma, in Ssreflect.seq]
sub_count [lemma, in Ssreflect.seq]
sub_has [lemma, in Ssreflect.seq]
sub_find [lemma, in Ssreflect.seq]
sub_ordK [lemma, in Ssreflect.fintype]
sub_ord [definition, in Ssreflect.fintype]
sub_ord_proof [lemma, in Ssreflect.fintype]
sub_enum_uniq [lemma, in Ssreflect.fintype]
sub_enum [definition, in Ssreflect.fintype]
sub_proper_trans [lemma, in Ssreflect.fintype]
sub_in21 [lemma, in Ssreflect.ssrbool]
sub_in12 [lemma, in Ssreflect.ssrbool]
sub_in3 [lemma, in Ssreflect.ssrbool]
sub_in2 [lemma, in Ssreflect.ssrbool]
sub_in_bij [lemma, in Ssreflect.ssrbool]
sub_in111 [lemma, in Ssreflect.ssrbool]
sub_in11 [lemma, in Ssreflect.ssrbool]
sub_in1 [lemma, in Ssreflect.ssrbool]
sub_refl [lemma, in Ssreflect.ssrbool]
sub_mem [definition, in Ssreflect.ssrbool]
sub0n [lemma, in Ssreflect.ssrnat]
sub0seq [lemma, in Ssreflect.seq]
sub1b [lemma, in Ssreflect.ssrnat]
sub1seq [lemma, in Ssreflect.seq]
succn [abbreviation, in Ssreflect.ssrnat]
succnK [lemma, in Ssreflect.ssrnat]
succn_inj [lemma, in Ssreflect.ssrnat]
suffix_subseq [lemma, in Ssreflect.seq]
sumboolP [lemma, in Ssreflect.ssrbool]
SumEqType [section, in Ssreflect.eqtype]
SumEqType.T1 [variable, in Ssreflect.eqtype]
SumEqType.T2 [variable, in Ssreflect.eqtype]
SumFinType [section, in Ssreflect.fintype]
SumFinType.T1 [variable, in Ssreflect.fintype]
SumFinType.T2 [variable, in Ssreflect.fintype]
sumn [definition, in Ssreflect.seq]
sumn_cat [lemma, in Ssreflect.seq]
sumn_nseq [lemma, in Ssreflect.seq]
sum_countType [definition, in Ssreflect.choice]
sum_countMixin [definition, in Ssreflect.choice]
sum_choiceType [definition, in Ssreflect.choice]
sum_choiceMixin [definition, in Ssreflect.choice]
sum_of_opair [definition, in Ssreflect.choice]
sum_eqE [lemma, in Ssreflect.eqtype]
sum_eqType [definition, in Ssreflect.eqtype]
sum_eqMixin [definition, in Ssreflect.eqtype]
sum_eqP [lemma, in Ssreflect.eqtype]
sum_eq [definition, in Ssreflect.eqtype]
sum_finType [definition, in Ssreflect.fintype]
sum_finMixin [definition, in Ssreflect.fintype]
sum_enum_uniq [lemma, in Ssreflect.fintype]
sum_enum [definition, in Ssreflect.fintype]
sval [abbreviation, in Ssreflect.ssrfun]
sval [abbreviation, in Ssreflect.eqtype]
svalP [lemma, in Ssreflect.ssrfun]
svalP [lemma, in Ssreflect.eqtype]
symmetric [definition, in Ssreflect.ssrbool]
symmetric_from_pre [lemma, in Ssreflect.ssrbool]
sym_right_transitive [lemma, in Ssreflect.ssrbool]
sym_left_transitive [lemma, in Ssreflect.ssrbool]
s2val [definition, in Ssreflect.ssrfun]
s2val [definition, in Ssreflect.eqtype]
s2valP [lemma, in Ssreflect.ssrfun]
s2valP [lemma, in Ssreflect.eqtype]
s2valP' [lemma, in Ssreflect.ssrfun]
s2valP' [lemma, in Ssreflect.eqtype]



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)