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 (72814 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 (1040 entries)
Binder 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 (47171 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 (791 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 (1547 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 (586 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 (11720 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 (1029 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 (625 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 (307 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 (474 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 (492 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 (896 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 (1648 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 (4323 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 (165 entries)

S (abbreviation)

sequence_minorant [in Coq.Reals.SeqProp]
sequence_majorant [in Coq.Reals.SeqProp]
SetoidFunctionalChoice [in Coq.Logic.ChoiceFacts]
set_digit [in Coq.Numbers.Cyclic.Int63.Int63]
shiftl [in Coq.Numbers.Natural.Peano.NPeano]
shiftl_spec_low [in Coq.Numbers.Natural.Peano.NPeano]
shiftl_spec_high [in Coq.Numbers.Natural.Peano.NPeano]
shiftr [in Coq.Numbers.Natural.Peano.NPeano]
shiftr_spec [in Coq.Numbers.Natural.Peano.NPeano]
SimpleSetoidFunctionalChoice [in Coq.Logic.ChoiceFacts]
sin3PI4 [in Coq.Reals.Rtrigo_calc]
sixteen [in Coq.Init.Nat]
size [in Coq.Numbers.Cyclic.Int63.Int63]
skipn_none [in Coq.Lists.List]
Snd [in Coq.Classes.RelationPairs]
sndT [in Coq.Init.Datatypes]
some [in Coq.ssr.ssrfun]
sort [in Coq.Sorting.Sorted]
SortA [in Coq.Lists.SetoidList]
sort_rect [in Coq.Sorting.Sorted]
sort_inv [in Coq.Sorting.Sorted]
Sort.Sorted [in Coq.Sorting.Mergesort]
sqrt [in Coq.Numbers.Natural.Peano.NPeano]
sqrt [in Coq.Numbers.Cyclic.Int63.Int63]
sqrt_spec [in Coq.Numbers.Natural.Peano.NPeano]
sqrt_iter_spec [in Coq.Numbers.Natural.Peano.NPeano]
sqrt_iter [in Coq.Numbers.Natural.Peano.NPeano]
sqrt_spec [in Coq.Numbers.Cyclic.Int63.Int63]
sqrt_init [in Coq.Numbers.Cyclic.Int63.Int63]
sqrt_step_correct [in Coq.Numbers.Cyclic.Int63.Int63]
sqrt_test_true [in Coq.Numbers.Cyclic.Int63.Int63]
sqrt_test_false [in Coq.Numbers.Cyclic.Int63.Int63]
sqrt_main [in Coq.Numbers.Cyclic.Int63.Int63]
sqrt_main_trick [in Coq.Numbers.Cyclic.Int63.Int63]
sqrt_step [in Coq.Numbers.Cyclic.Int63.Int63]
sqrt2 [in Coq.Numbers.Cyclic.Int63.Int63]
sqrt2_spec [in Coq.Numbers.Cyclic.Int63.Int63]
sqrt2_step_correct [in Coq.Numbers.Cyclic.Int63.Int63]
sqrt2_lower_bound [in Coq.Numbers.Cyclic.Int63.Int63]
sqrt2_step_def [in Coq.Numbers.Cyclic.Int63.Int63]
sqrt2_step [in Coq.Numbers.Cyclic.Int63.Int63]
square [in Coq.Numbers.Natural.Peano.NPeano]
square_spec [in Coq.Numbers.Natural.Peano.NPeano]
SsrMatchingSyntax.LHS [in Coq.ssrmatching.ssrmatching]
SsrMatchingSyntax.RHS [in Coq.ssrmatching.ssrmatching]
Step [in Coq.NArith.Ndigits]
Stream [in Coq.Lists.Streams]
sub [in Coq.Numbers.Cyclic.Int63.Int63]
sub [in Coq.Numbers.Cyclic.Int63.Uint63]
subc [in Coq.Numbers.Cyclic.Int63.Int63]
subc [in Coq.Numbers.Cyclic.Int63.Uint63]
subcarry [in Coq.Numbers.Cyclic.Int63.Int63]
subcarryc [in Coq.Numbers.Cyclic.Int63.Int63]
subcarryc [in Coq.Numbers.Cyclic.Int63.Uint63]
subcarryc_spec [in Coq.Numbers.Cyclic.Int63.Int63]
subcarryc_def_spec [in Coq.Numbers.Cyclic.Int63.Int63]
subcarryc_def [in Coq.Numbers.Cyclic.Int63.Int63]
subcarry_spec [in Coq.Numbers.Cyclic.Int63.Int63]
subc_spec [in Coq.Numbers.Cyclic.Int63.Int63]
subc_def_spec [in Coq.Numbers.Cyclic.Int63.Int63]
subc_def [in Coq.Numbers.Cyclic.Int63.Int63]
sub_spec [in Coq.Numbers.Cyclic.Int63.Int63]
succ [in Coq.Numbers.Cyclic.Int63.Int63]
succc [in Coq.Numbers.Cyclic.Int63.Int63]
succc_spec [in Coq.Numbers.Cyclic.Int63.Int63]
succ_spec [in Coq.Numbers.Cyclic.Int63.Int63]
succ_plus_discr [in Coq.Arith.Plus]
succ_min_distr [in Coq.Arith.Min]
succ_max_distr [in Coq.Arith.Max]
sval [in Coq.ssr.ssrfun]
SwapProd [in Coq.Wellfounded.Lexicographic_Product]
Symprod [in Coq.Wellfounded.Lexicographic_Product]
sym_JMeq [in Coq.Logic.JMeq]
sym_not_id [in Coq.Init.Datatypes]
sym_id [in Coq.Init.Datatypes]
sym_not_equal [in Coq.Init.Logic]
sym_equal [in Coq.Init.Logic]
sym_not_eq [in Coq.Init.Logic]
sym_eq [in Coq.Init.Logic]
SYM1 [in Coq.ZArith.BinInt]
SYM2 [in Coq.ZArith.BinInt]
SYM3 [in Coq.ZArith.BinInt]
S_pred_pos [in Coq.Arith.Lt]
S_pred [in Coq.Arith.Lt]



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 (72814 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 (1040 entries)
Binder 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 (47171 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 (791 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 (1547 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 (586 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 (11720 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 (1029 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 (625 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 (307 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 (474 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 (492 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 (896 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 (1648 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 (4323 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 (165 entries)