Standard Library | The Coq Proof Assistant

Global Index

(73252 entries)

Notation Index

F

J

K

T

X

Y

_

(1016 entries)

Binder Index

_

other

(47569 entries)

Module Index

J

X

Y

_

other

(800 entries)

Variable Index

J

Q

V

X

Y

_

other

(1555 entries)

Library Index

K

X

Y

_

other

(592 entries)

Lemma Index

other

(11846 entries)

Constructor Index

K

Y

_

other

(959 entries)

Axiom Index

J

K

V

X

Y

_

other

(629 entries)

Inductive Index

X

Y

_

other

(308 entries)

Projection Index

G

K

V

X

Y

_

other

(475 entries)

Section Index

J

Q

X

Y

_

other

(494 entries)

Instance Index

J

V

X

Y

_

other

(912 entries)

Abbreviation Index

J

Y

_

other

(1503 entries)

Definition Index

_

other

(4428 entries)

Record Index

J

V

X

Y

_

other

(166 entries)

S (definition)

Same_set [in Coq.Sets.Ensembles]
same_relation [in Coq.Sets.Relations_1]
same_relation [in Coq.Relations.Relation_Definitions]
Sdep.Add [in Coq.FSets.FSetInterface]
Sdep.elt [in Coq.FSets.FSetInterface]
Sdep.Empty [in Coq.FSets.FSetInterface]
Sdep.eq [in Coq.FSets.FSetInterface]
Sdep.Equal [in Coq.FSets.FSetInterface]
Sdep.Exists [in Coq.FSets.FSetInterface]
Sdep.For_all [in Coq.FSets.FSetInterface]
Sdep.Subset [in Coq.FSets.FSetInterface]
self_inverse [in Coq.ssr.ssrfun]
seq [in Coq.Lists.List]
seq [in Coq.Sets.Uniset]
sequence_lb [in Coq.Reals.SeqProp]
sequence_ub [in Coq.Reals.SeqProp]
seq_cv [in Coq.Reals.Cauchy.ConstructiveRcomplete]
Seq_trans [in Coq.Setoids.Setoid]
Seq_sym [in Coq.Setoids.Setoid]
Seq_refl [in Coq.Setoids.Setoid]
series_cv_abs [in Coq.Reals.Abstract.ConstructiveSum]
series_cv_le_lim [in Coq.Reals.Abstract.ConstructiveSum]
series_cv_lim_lt [in Coq.Reals.Abstract.ConstructiveSum]
series_cv [in Coq.Reals.Abstract.ConstructiveSum]
set [in Coq.Lists.ListSet]
Setminus [in Coq.Sets.Ensembles]
SetoidFunctionalChoice_on [in Coq.Logic.ChoiceFacts]
setoid_trans [in Coq.Classes.SetoidClass]
setoid_sym [in Coq.Classes.SetoidClass]
setoid_refl [in Coq.Classes.SetoidClass]
Setoid_Theory [in Coq.Setoids.Setoid]
set_map [in Coq.Lists.ListSet]
set_fold_right [in Coq.Lists.ListSet]
set_fold_left [in Coq.Lists.ListSet]
set_power [in Coq.Lists.ListSet]
set_prod [in Coq.Lists.ListSet]
set_In [in Coq.Lists.ListSet]
set_diff [in Coq.Lists.ListSet]
set_union [in Coq.Lists.ListSet]
set_inter [in Coq.Lists.ListSet]
set_remove [in Coq.Lists.ListSet]
set_mem [in Coq.Lists.ListSet]
set_add [in Coq.Lists.ListSet]
set_digit [in Coq.Numbers.Cyclic.Int63.Uint63]
SFabs [in Coq.Floats.SpecFloat]
SFadd [in Coq.Floats.SpecFloat]
SFclassify [in Coq.Floats.SpecFloat]
SFcompare [in Coq.Floats.SpecFloat]
SFdiv [in Coq.Floats.SpecFloat]
SFdiv_core_binary [in Coq.Floats.SpecFloat]
SFeqb [in Coq.Floats.SpecFloat]
SFfrexp [in Coq.Floats.SpecFloat]
SFL [in Coq.Reals.PSeries_reg]
SFldexp [in Coq.Floats.SpecFloat]
SFleb [in Coq.Floats.SpecFloat]
SFltb [in Coq.Floats.SpecFloat]
SFmax_float [in Coq.Floats.SpecFloat]
SFmul [in Coq.Floats.SpecFloat]
SFnormfr_mantissa [in Coq.Floats.SpecFloat]
SFone [in Coq.Floats.SpecFloat]
SFopp [in Coq.Floats.SpecFloat]
SFpred [in Coq.Floats.SpecFloat]
SFpred_pos [in Coq.Floats.SpecFloat]
SFsqrt [in Coq.Floats.SpecFloat]
SFsqrt_core_binary [in Coq.Floats.SpecFloat]
SFsub [in Coq.Floats.SpecFloat]
SFsucc [in Coq.Floats.SpecFloat]
SFulp [in Coq.Floats.SpecFloat]
Sfun.lt_key [in Coq.FSets.FMapInterface]
SF2AF [in Coq.setoid_ring.Field_theory]
SF2Prim [in Coq.Floats.FloatOps]
SF64add [in Coq.Floats.FloatAxioms]
SF64classify [in Coq.Floats.FloatAxioms]
SF64div [in Coq.Floats.FloatAxioms]
SF64mul [in Coq.Floats.FloatAxioms]
SF64pred [in Coq.Floats.FloatAxioms]
SF64sqrt [in Coq.Floats.FloatAxioms]
SF64sub [in Coq.Floats.FloatAxioms]
SF64succ [in Coq.Floats.FloatAxioms]
shift [in Coq.Floats.FloatOps]
shift [in Coq.ZArith.Zpower]
shift [in Coq.Strings.Ascii]
shiftin [in Coq.Vectors.VectorDef]
shiftl [in Coq.Init.Nat]
shiftl [in Coq.Numbers.Cyclic.Int31.Int31]
shiftout [in Coq.Vectors.VectorDef]
shiftr [in Coq.Init.Nat]
shiftr [in Coq.Numbers.Cyclic.Int31.Int31]
shiftrepeat [in Coq.Vectors.VectorDef]
shift_pos [in Coq.ZArith.Zpower]
shift_nat [in Coq.ZArith.Zpower]
shl_align [in Coq.Floats.SpecFloat]
shr [in Coq.Floats.SpecFloat]
shr_fexp [in Coq.Floats.SpecFloat]
shr_record_of_loc [in Coq.Floats.SpecFloat]
shr_1 [in Coq.Floats.SpecFloat]
sigma [in Coq.Reals.Rsigma]
sigT_of_sigT2_eq [in Coq.Init.Specif]
sigT_of_prod [in Coq.Init.Specif]
sigT_eta [in Coq.Init.Specif]
sigT_of_sig [in Coq.Init.Specif]
sigT_of_sigT2 [in Coq.Init.Specif]
sigT2_eta [in Coq.Init.Specif]
sigT2_of_sig2 [in Coq.Init.Specif]
sig_not_dec_T [in Coq.Reals.Abstract.ConstructiveLUB]
sig_forall_dec_T [in Coq.Reals.Abstract.ConstructiveLUB]
sig_of_sig2_eq [in Coq.Init.Specif]
sig_eta [in Coq.Init.Specif]
sig_of_sigT [in Coq.Init.Specif]
sig_of_sig2 [in Coq.Init.Specif]
sig_of_sig2 [in Coq.ssr.ssrfun]
sig2_eta [in Coq.Init.Specif]
sig2_of_sigT2 [in Coq.Init.Specif]
SimpleMergeExample [in Coq.Sorting.Mergesort]
SimpleSetoidFunctionalChoice_on [in Coq.Logic.ChoiceFacts]
SimplFunDelta [in Coq.ssr.ssrfun]
SimplPred [in Coq.ssr.ssrbool]
simplPredType [in Coq.ssr.ssrbool]
SimplRel [in Coq.ssr.ssrbool]
simpl_cone [in Coq.micromega.RingMicromega]
simpl_of_mem [in Coq.ssr.ssrbool]
simpl_rel [in Coq.ssr.ssrbool]
simpl_pred [in Coq.ssr.ssrbool]
sin [in Coq.Reals.Rtrigo_def]
sind [in Coq.Reals.Rtrigo_calc]
Singleton [in Coq.Sets.Uniset]
singleton [in Coq.micromega.VarMap]
SingletonBag [in Coq.Sets.Multiset]
sinh [in Coq.Reals.Rtrigo_def]
sin_in [in Coq.Reals.Rtrigo_def]
sin_n [in Coq.Reals.Rtrigo_def]
sin_ub [in Coq.Reals.Rtrigo1]
sin_lb [in Coq.Reals.Rtrigo1]
sin_approx [in Coq.Reals.Rtrigo_alt]
sin_term [in Coq.Reals.Rtrigo_alt]
size [in Coq.Numbers.Cyclic.Int31.Int31]
size [in Coq.Numbers.Cyclic.Int63.Uint63]
skipn [in Coq.Lists.List]
SlowConstructiveRealsMorphism [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
SlowMorph [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
SmallDrinker'sParadox [in Coq.Logic.ChoiceFacts]
snd [in Coq.Init.Datatypes]
sneakl [in Coq.Numbers.Cyclic.Int31.Int31]
sneakr [in Coq.Numbers.Cyclic.Int31.Int31]
sol_x2 [in Coq.Reals.R_sqrt]
sol_x1 [in Coq.Reals.R_sqrt]
Sord.cmp [in Coq.FSets.FMapInterface]
Sord.t [in Coq.FSets.FMapInterface]
Sort.flatten_stack [in Coq.Sorting.Mergesort]
Sort.iter_merge [in Coq.Sorting.Mergesort]
Sort.merge [in Coq.Sorting.Mergesort]
Sort.merge_stack [in Coq.Sorting.Mergesort]
Sort.merge_list_to_stack [in Coq.Sorting.Mergesort]
Sort.sort [in Coq.Sorting.Mergesort]
Sort.SortedStack [in Coq.Sorting.Mergesort]
SP [in Coq.Reals.PartSum]
Space [in Coq.Strings.Ascii]
split [in Coq.Lists.List]
split [in Coq.setoid_ring.Field_theory]
splitat [in Coq.Vectors.VectorDef]
split_aux [in Coq.setoid_ring.Field_theory]
sqrt [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
sqrt [in Coq.Reals.R_sqrt]
sqrt [in Coq.Init.Nat]
sqrt [in Coq.Numbers.Cyclic.Int63.Uint63]
sqrt_iter [in Coq.Init.Nat]
sqrt_step [in Coq.Numbers.Cyclic.Int63.Uint63]
sqrt2 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
sqrt2 [in Coq.Numbers.Cyclic.Int63.Uint63]
sqrt2_step [in Coq.Numbers.Cyclic.Int63.Uint63]
sqrt31 [in Coq.Numbers.Cyclic.Int31.Int31]
sqrt31_step [in Coq.Numbers.Cyclic.Int31.Int31]
sqrt312 [in Coq.Numbers.Cyclic.Int31.Int31]
sqrt312_step [in Coq.Numbers.Cyclic.Int31.Int31]
square [in Coq.Init.Nat]
square_c [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
SRIDmorph [in Coq.setoid_ring.Ring_theory]
SRopp [in Coq.setoid_ring.Ring_theory]
SRsub [in Coq.setoid_ring.Ring_theory]
ssr_converse [in Coq.ssr.ssreflect]
Streicher_K_ [in Coq.Logic.EqdepFacts]
Streicher_K_on_ [in Coq.Logic.EqdepFacts]
strict_decreasing [in Coq.Reals.Ranalysis1]
strict_increasing [in Coq.Reals.Ranalysis1]
Strict_Included [in Coq.Sets.Ensembles]
Strict_Rel_of [in Coq.Sets.Partial_Order]
String_as_OT.lt [in Coq.Structures.OrdersEx]
String_as_OT.compare [in Coq.Structures.OrdersEx]
String_as_OT.eqb_eq [in Coq.Structures.OrdersEx]
String_as_OT.eqb [in Coq.Structures.OrdersEx]
String_as_OT.t [in Coq.Structures.OrdersEx]
string_of_list_byte [in Coq.Strings.String]
string_of_list_ascii [in Coq.Strings.String]
string_dec [in Coq.Strings.String]
String_as_OT.eq_dec [in Coq.Structures.OrderedTypeEx]
String_as_OT.compare [in Coq.Structures.OrderedTypeEx]
String_as_OT.cmp [in Coq.Structures.OrderedTypeEx]
String_as_OT.lt [in Coq.Structures.OrderedTypeEx]
String_as_OT.eq_trans [in Coq.Structures.OrderedTypeEx]
String_as_OT.eq_sym [in Coq.Structures.OrderedTypeEx]
String_as_OT.eq_refl [in Coq.Structures.OrderedTypeEx]
String_as_OT.eq [in Coq.Structures.OrderedTypeEx]
String_as_OT.t [in Coq.Structures.OrderedTypeEx]
Strongly_confluent [in Coq.Sets.Relations_2]
Str_nth [in Coq.Lists.Streams]
Str_nth_tl [in Coq.Lists.Streams]
sub [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
sub [in Coq.Init.Nat]
subcarry [in Coq.Numbers.Cyclic.Int63.Uint63]
subcarryc_def [in Coq.Numbers.Cyclic.Int63.Uint63]
subc_def [in Coq.Numbers.Cyclic.Int63.Uint63]
subdivision [in Coq.Reals.RiemannInt_SF]
subdivision_val [in Coq.Reals.RiemannInt_SF]
SubEqui [in Coq.Reals.RiemannInt]
SubEquiN [in Coq.Reals.RiemannInt]
subfamily [in Coq.Reals.Rtopology]
subpred [in Coq.ssr.ssrbool]
subrel [in Coq.ssr.ssrbool]
subrelation [in Coq.Init.Logic]
subset [in Coq.Logic.ClassicalChoice]
substring [in Coq.Strings.String]
Subtract [in Coq.Sets.Ensembles]
sub_carry [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
sub_carry_c [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
sub_c [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
sub_mem [in Coq.ssr.ssrbool]
sub31 [in Coq.Numbers.Cyclic.Int31.Int31]
sub31c [in Coq.Numbers.Cyclic.Int31.Int31]
sub31carryc [in Coq.Numbers.Cyclic.Int31.Int31]
succ [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
succ [in Coq.Init.Nat]
succ [in Coq.Numbers.Cyclic.Int63.Uint63]
succc [in Coq.Numbers.Cyclic.Int63.Uint63]
succ_c [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
sumboolb [in Coq.micromega.RMicromega]
sumbool_not [in Coq.Bool.Sumbool]
sumbool_or [in Coq.Bool.Sumbool]
sumbool_and [in Coq.Bool.Sumbool]
sumbool_of_bool [in Coq.Bool.Sumbool]
sum_f [in Coq.Reals.Rfunctions]
sum_f_R0 [in Coq.Reals.Rfunctions]
sum_nat [in Coq.Reals.Rfunctions]
sum_nat_O [in Coq.Reals.Rfunctions]
sum_nat_f [in Coq.Reals.Rfunctions]
sum_nat_f_O [in Coq.Reals.Rfunctions]
Surjective [in Coq.Logic.FinFun]
swap_sumbool [in Coq.Classes.EquivDec]
swap_sumbool [in Coq.Classes.SetoidDec]
symmetric [in Coq.ssr.ssrbool]
Symmetric [in Coq.Sets.Relations_1]
symmetric [in Coq.Relations.Relation_Definitions]
S_pred_pos_stt [in Coq.Arith.Lt]
S_pred_stt [in Coq.Arith.Lt]
s2val [in Coq.ssr.ssrfun]

Global Index

(73252 entries)

Notation Index

F

J

K

T

X

Y

_

(1016 entries)

Binder Index

_

other

(47569 entries)

Module Index

J

X

Y

_

other

(800 entries)

Variable Index

J

Q

V

X

Y

_

other

(1555 entries)

Library Index

K

X

Y

_

other

(592 entries)

Lemma Index

other

(11846 entries)

Constructor Index

K

Y

_

other

(959 entries)

Axiom Index

J

K

V

X

Y

_

other

(629 entries)

Inductive Index

X

Y

_

other

(308 entries)

Projection Index

G

K

V

X

Y

_

other

(475 entries)

Section Index

J

Q

X

Y

_

other

(494 entries)

Instance Index

J

V

X

Y

_

other

(912 entries)

Abbreviation Index

J

Y

_

other

(1503 entries)

Definition Index

_

other

(4428 entries)

Record Index

J

V

X

Y

_

other

(166 entries)