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

(3486 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

(293 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

(51 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

(312 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

(100 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

(435 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

(611 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

(149 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

(99 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

(76 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

(117 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

(111 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

(108 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

(962 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

(62 entries)

---

S

S [constructor, in Corelib.Init.Datatypes]
sameP [lemma, in Corelib.ssr.ssrbool]
same_relation [definition, in Corelib.Relations.Relation_Definitions]
self_inverse [definition, in Corelib.ssr.ssrfun]
seq [definition, in Corelib.Lists.ListDef]
Seq_trans [definition, in Corelib.Setoids.Setoid]
Seq_sym [definition, in Corelib.Setoids.Setoid]
Seq_refl [definition, in Corelib.Setoids.Setoid]
set [axiom, in Corelib.Array.PrimArray]
Setoid [library]
SetoidTactics [library]
Setoid_Theory [definition, in Corelib.Setoids.Setoid]
set_digit [definition, in Corelib.Numbers.Cyclic.Int63.Uint63Axioms]
SFabs [definition, in Corelib.Floats.SpecFloat]
SFadd [definition, in Corelib.Floats.SpecFloat]
SFclassify [definition, in Corelib.Floats.SpecFloat]
SFcompare [definition, in Corelib.Floats.SpecFloat]
SFdiv [definition, in Corelib.Floats.SpecFloat]
SFdiv_core_binary [definition, in Corelib.Floats.SpecFloat]
SFeqb [definition, in Corelib.Floats.SpecFloat]
SFfrexp [definition, in Corelib.Floats.SpecFloat]
SFldexp [definition, in Corelib.Floats.SpecFloat]
SFleb [definition, in Corelib.Floats.SpecFloat]
SFltb [definition, in Corelib.Floats.SpecFloat]
SFmax_float [definition, in Corelib.Floats.SpecFloat]
SFmul [definition, in Corelib.Floats.SpecFloat]
SFnormfr_mantissa [definition, in Corelib.Floats.SpecFloat]
SFone [definition, in Corelib.Floats.SpecFloat]
SFopp [definition, in Corelib.Floats.SpecFloat]
SFpred [definition, in Corelib.Floats.SpecFloat]
SFpred_pos [definition, in Corelib.Floats.SpecFloat]
SFsqrt [definition, in Corelib.Floats.SpecFloat]
SFsqrt_core_binary [definition, in Corelib.Floats.SpecFloat]
SFsub [definition, in Corelib.Floats.SpecFloat]
SFsucc [definition, in Corelib.Floats.SpecFloat]
SFulp [definition, in Corelib.Floats.SpecFloat]
SF2Prim [definition, in Corelib.Floats.FloatOps]
SF2Prim_inj [lemma, in Corelib.Floats.FloatAxioms]
SF2Prim_Prim2SF [axiom, in Corelib.Floats.FloatAxioms]
SF64add [definition, in Corelib.Floats.FloatAxioms]
SF64classify [definition, in Corelib.Floats.FloatAxioms]
SF64div [definition, in Corelib.Floats.FloatAxioms]
SF64mul [definition, in Corelib.Floats.FloatAxioms]
SF64pred [definition, in Corelib.Floats.FloatAxioms]
SF64sqrt [definition, in Corelib.Floats.FloatAxioms]
SF64sub [definition, in Corelib.Floats.FloatAxioms]
SF64succ [definition, in Corelib.Floats.FloatAxioms]
shift [definition, in Corelib.Floats.FloatOps]
shiftl [definition, in Corelib.Init.Nat]
shiftr [definition, in Corelib.Init.Nat]
shl_align [definition, in Corelib.Floats.SpecFloat]
shr [definition, in Corelib.Floats.SpecFloat]
shr_fexp [definition, in Corelib.Floats.SpecFloat]
shr_record_of_loc [definition, in Corelib.Floats.SpecFloat]
shr_1 [definition, in Corelib.Floats.SpecFloat]
shr_s [projection, in Corelib.Floats.SpecFloat]
shr_r [projection, in Corelib.Floats.SpecFloat]
shr_m [projection, in Corelib.Floats.SpecFloat]
shr_record [record, in Corelib.Floats.SpecFloat]
sig [section, in Corelib.Init.Specif]
sig [inductive, in Corelib.Init.Specif]
Sig [section, in Corelib.ssr.ssrfun]
signed_int_eq_dec [definition, in Corelib.Init.Hexadecimal]
signed_int [inductive, in Corelib.Init.Hexadecimal]
signed_int_eq_dec [definition, in Corelib.Init.Decimal]
signed_int [inductive, in Corelib.Init.Decimal]
signed_int_eq_dec [definition, in Corelib.Init.Number]
signed_int [inductive, in Corelib.Init.Number]
sigT [section, in Corelib.Init.Specif]
sigT [inductive, in Corelib.Init.Specif]
SigTNotations [module, in Corelib.Init.Specif]
_ .2 [notation, in Corelib.Init.Specif]
_ .1 [notation, in Corelib.Init.Specif]
( _ ; _ ) [notation, in Corelib.Init.Specif]
sigT_of_sigT2_eq [definition, in Corelib.Init.Specif]
sigT_prod_sigT [lemma, in Corelib.Init.Specif]
sigT_of_prod [definition, in Corelib.Init.Specif]
sigT_eta [definition, in Corelib.Init.Specif]
sigT_of_sig [definition, in Corelib.Init.Specif]
sigT_of_sigT2 [definition, in Corelib.Init.Specif]
sigT_sind [definition, in Corelib.Init.Specif]
sigT_rec [definition, in Corelib.Init.Specif]
sigT_ind [definition, in Corelib.Init.Specif]
sigT_rect [definition, in Corelib.Init.Specif]
(= _ ; _ ) [notation, in Corelib.Init.Specif]
sigT2 [section, in Corelib.Init.Specif]
sigT2 [inductive, in Corelib.Init.Specif]
sigT2_eta [definition, in Corelib.Init.Specif]
sigT2_of_sig2 [definition, in Corelib.Init.Specif]
sigT2_sind [definition, in Corelib.Init.Specif]
sigT2_rec [definition, in Corelib.Init.Specif]
sigT2_ind [definition, in Corelib.Init.Specif]
sigT2_rect [definition, in Corelib.Init.Specif]
sig_of_sig2_eq [definition, in Corelib.Init.Specif]
sig_eta [definition, in Corelib.Init.Specif]
sig_of_sigT [definition, in Corelib.Init.Specif]
sig_of_sig2 [definition, in Corelib.Init.Specif]
sig_sind [definition, in Corelib.Init.Specif]
sig_rec [definition, in Corelib.Init.Specif]
sig_ind [definition, in Corelib.Init.Specif]
sig_rect [definition, in Corelib.Init.Specif]
sig_of_sig2 [definition, in Corelib.ssr.ssrfun]
Sig.P [variable, in Corelib.ssr.ssrfun]
Sig.Q [variable, in Corelib.ssr.ssrfun]
Sig.T [variable, in Corelib.ssr.ssrfun]
sig2 [section, in Corelib.Init.Specif]
sig2 [inductive, in Corelib.Init.Specif]
sig2_eta [definition, in Corelib.Init.Specif]
sig2_of_sigT2 [definition, in Corelib.Init.Specif]
sig2_sind [definition, in Corelib.Init.Specif]
sig2_rec [definition, in Corelib.Init.Specif]
sig2_ind [definition, in Corelib.Init.Specif]
sig2_rect [definition, in Corelib.Init.Specif]
SimplFun [section, in Corelib.ssr.ssrfun]
SimplFun [constructor, in Corelib.ssr.ssrfun]
SimplFunDelta [definition, in Corelib.ssr.ssrfun]
SimplFun.aT [variable, in Corelib.ssr.ssrfun]
SimplFun.rT [variable, in Corelib.ssr.ssrfun]
SimplPred [definition, in Corelib.ssr.ssrbool]
simplPredType [definition, in Corelib.ssr.ssrbool]
SimplRel [definition, in Corelib.ssr.ssrbool]
simpl_predE [lemma, in Corelib.ssr.ssrbool]
simpl_pred_value [projection, in Corelib.ssr.ssrbool]
simpl_of_mem [definition, in Corelib.ssr.ssrbool]
simpl_rel [definition, in Corelib.ssr.ssrbool]
simpl_pred [definition, in Corelib.ssr.ssrbool]
simpl_fun [inductive, in Corelib.ssr.ssrfun]
Sint63Axioms [library]
sixteen [abbreviation, in Corelib.Init.Nat]
size [definition, in Corelib.Numbers.Cyclic.Int63.Uint63Axioms]
skipn [definition, in Corelib.Lists.ListDef]
snd [definition, in Corelib.Init.Datatypes]
sndT [abbreviation, in Corelib.Init.Datatypes]
Some [constructor, in Corelib.Init.Datatypes]
some [abbreviation, in Corelib.ssr.ssrfun]
Some_inj [lemma, in Corelib.ssr.ssrfun]
SpecFloat [library]
Specif [library]
spec_float [inductive, in Corelib.Floats.SpecFloat]
sqrt [definition, in Corelib.Init.Nat]
sqrt [axiom, in Corelib.Floats.PrimFloat]
sqrt_spec [axiom, in Corelib.Floats.FloatAxioms]
sqrt_iter [definition, in Corelib.Init.Nat]
square [definition, in Corelib.Init.Nat]
ssrbool [library]
ssrclasses [library]
ssreflect [library]
ssrfun [library]
ssrmatching [library]
SsrMatchingSyntax [module, in Corelib.ssrmatching.ssrmatching]
SsrMatchingSyntax.LHS [abbreviation, in Corelib.ssrmatching.ssrmatching]
SsrMatchingSyntax.RHS [abbreviation, in Corelib.ssrmatching.ssrmatching]
( _ in _ ) (ssrpatternscope) [notation, in Corelib.ssrmatching.ssrmatching]
ssrsetoid [library]
SsrSyntax [module, in Corelib.ssr.ssreflect]
ssrunder [library]
ssr_congr_arrow [lemma, in Corelib.ssr.ssreflect]
ssr_have_upoly [lemma, in Corelib.ssr.ssreflect]
ssr_have [lemma, in Corelib.ssr.ssreflect]
ssr_converse [definition, in Corelib.ssr.ssreflect]
Std [library]
StrictOrder [record, in Corelib.Classes.RelationClasses]
StrictOrder [record, in Corelib.Classes.CRelationClasses]
StrictOrder_Asymmetric [instance, in Corelib.Classes.RelationClasses]
StrictOrder_Transitive [projection, in Corelib.Classes.RelationClasses]
StrictOrder_Irreflexive [projection, in Corelib.Classes.RelationClasses]
StrictOrder_PartialOrder [lemma, in Corelib.Classes.CMorphisms]
StrictOrder_PreOrder [lemma, in Corelib.Classes.CMorphisms]
StrictOrder_PartialOrder [lemma, in Corelib.Classes.Morphisms]
StrictOrder_PreOrder [lemma, in Corelib.Classes.Morphisms]
StrictOrder_Asymmetric [instance, in Corelib.Classes.CRelationClasses]
StrictOrder_Transitive [projection, in Corelib.Classes.CRelationClasses]
StrictOrder_Irreflexive [projection, in Corelib.Classes.CRelationClasses]
string [axiom, in Corelib.Strings.PrimString]
String [library]
sub [definition, in Corelib.Init.Nat]
sub [axiom, in Corelib.Strings.PrimString]
sub [axiom, in Corelib.Floats.PrimFloat]
sub [axiom, in Corelib.Numbers.Cyclic.Int63.PrimInt63]
subc [axiom, in Corelib.Numbers.Cyclic.Int63.PrimInt63]
subcarryc [axiom, in Corelib.Numbers.Cyclic.Int63.PrimInt63]
subcarryc_def_spec [axiom, in Corelib.Numbers.Cyclic.Int63.Uint63Axioms]
subcarryc_def [definition, in Corelib.Numbers.Cyclic.Int63.Uint63Axioms]
subc_def_spec [axiom, in Corelib.Numbers.Cyclic.Int63.Uint63Axioms]
subc_def [definition, in Corelib.Numbers.Cyclic.Int63.Uint63Axioms]
subon_bij [lemma, in Corelib.ssr.ssrbool]
subon1 [lemma, in Corelib.ssr.ssrbool]
subon1l [lemma, in Corelib.ssr.ssrbool]
subon2 [lemma, in Corelib.ssr.ssrbool]
subpred [definition, in Corelib.ssr.ssrbool]
subrel [definition, in Corelib.ssr.ssrbool]
subrelation [record, in Corelib.Classes.RelationClasses]
subrelation [inductive, in Corelib.Classes.RelationClasses]
subrelation [record, in Corelib.Classes.CRelationClasses]
subrelation [inductive, in Corelib.Classes.CRelationClasses]
subrelation [definition, in Corelib.Init.Logic]
subrelation_partial_order [instance, in Corelib.Classes.RelationClasses]
subrelation_symmetric [lemma, in Corelib.Classes.RelationClasses]
subrelation_proper [lemma, in Corelib.Classes.CMorphisms]
subrelation_refl [lemma, in Corelib.Classes.CMorphisms]
subrelation_respectful [lemma, in Corelib.Classes.CMorphisms]
subrelation_id_proper [instance, in Corelib.Classes.CMorphisms]
subrelation_proper [lemma, in Corelib.Classes.Morphisms]
subrelation_refl [lemma, in Corelib.Classes.Morphisms]
subrelation_respectful [lemma, in Corelib.Classes.Morphisms]
subrelation_id_proper [instance, in Corelib.Classes.Morphisms]
subrelation_symmetric [lemma, in Corelib.Classes.CRelationClasses]
subrelUl [lemma, in Corelib.ssr.ssrbool]
subrelUr [lemma, in Corelib.ssr.ssrbool]
Subset_projections2.Q [variable, in Corelib.Init.Specif]
Subset_projections2.P [variable, in Corelib.Init.Specif]
Subset_projections2.A [variable, in Corelib.Init.Specif]
Subset_projections2 [section, in Corelib.Init.Specif]
Subset_projections.P [variable, in Corelib.Init.Specif]
Subset_projections.A [variable, in Corelib.Init.Specif]
Subset_projections [section, in Corelib.Init.Specif]
sub_spec [axiom, in Corelib.Floats.FloatAxioms]
sub_in21 [lemma, in Corelib.ssr.ssrbool]
sub_in12 [lemma, in Corelib.ssr.ssrbool]
sub_in3 [lemma, in Corelib.ssr.ssrbool]
sub_in2 [lemma, in Corelib.ssr.ssrbool]
sub_in_bij [lemma, in Corelib.ssr.ssrbool]
sub_in111 [lemma, in Corelib.ssr.ssrbool]
sub_in11 [lemma, in Corelib.ssr.ssrbool]
sub_in1 [lemma, in Corelib.ssr.ssrbool]
sub_refl [lemma, in Corelib.ssr.ssrbool]
sub_mem [definition, in Corelib.ssr.ssrbool]
sub_spec [axiom, in Corelib.Numbers.Cyclic.Int63.Uint63Axioms]
sub_spec [axiom, in Corelib.Strings.PrimStringAxioms]
succ [definition, in Corelib.Init.Nat]
sum [inductive, in Corelib.Init.Datatypes]
sumbool [inductive, in Corelib.Init.Specif]
Sumbool [library]
sumboolP [lemma, in Corelib.ssr.ssrbool]
sumbool_sind [definition, in Corelib.Init.Specif]
sumbool_rec [definition, in Corelib.Init.Specif]
sumbool_ind [definition, in Corelib.Init.Specif]
sumbool_rect [definition, in Corelib.Init.Specif]
sumbool_not [definition, in Corelib.Init.Sumbool]
sumbool_or [definition, in Corelib.Init.Sumbool]
sumbool_and [definition, in Corelib.Init.Sumbool]
sumbool_of_bool [definition, in Corelib.Init.Sumbool]
sumor [inductive, in Corelib.Init.Specif]
sumor_sind [definition, in Corelib.Init.Specif]
sumor_rec [definition, in Corelib.Init.Specif]
sumor_ind [definition, in Corelib.Init.Specif]
sumor_rect [definition, in Corelib.Init.Specif]
sum_sind [definition, in Corelib.Init.Datatypes]
sum_rec [definition, in Corelib.Init.Datatypes]
sum_ind [definition, in Corelib.Init.Datatypes]
sum_rect [definition, in Corelib.Init.Datatypes]
surjective_pairing [lemma, in Corelib.Init.Datatypes]
sval [abbreviation, in Corelib.ssr.ssrfun]
svalP [lemma, in Corelib.ssr.ssrfun]
Symmetric [record, in Corelib.Classes.RelationClasses]
Symmetric [inductive, in Corelib.Classes.RelationClasses]
symmetric [definition, in Corelib.ssr.ssrbool]
Symmetric [record, in Corelib.Classes.CRelationClasses]
Symmetric [inductive, in Corelib.Classes.CRelationClasses]
symmetric [definition, in Corelib.Relations.Relation_Definitions]
symmetric_from_pre [lemma, in Corelib.ssr.ssrbool]
symmetric_equiv_flip [lemma, in Corelib.Classes.CMorphisms]
symmetric_equiv_flip [lemma, in Corelib.Classes.Morphisms]
symmetry [projection, in Corelib.Classes.RelationClasses]
symmetry [constructor, in Corelib.Classes.RelationClasses]
symmetry [projection, in Corelib.Classes.CRelationClasses]
symmetry [constructor, in Corelib.Classes.CRelationClasses]
sym_not_id [abbreviation, in Corelib.Init.Datatypes]
sym_id [abbreviation, in Corelib.Init.Datatypes]
sym_right_transitive [lemma, in Corelib.ssr.ssrbool]
sym_left_transitive [lemma, in Corelib.ssr.ssrbool]
sym_not_equal [abbreviation, in Corelib.Init.Logic]
sym_equal [abbreviation, in Corelib.Init.Logic]
sym_not_eq [abbreviation, in Corelib.Init.Logic]
sym_eq [abbreviation, in Corelib.Init.Logic]
s2val [definition, in Corelib.ssr.ssrfun]
s2valP [lemma, in Corelib.ssr.ssrfun]
s2valP' [lemma, in Corelib.ssr.ssrfun]
S754_finite [constructor, in Corelib.Floats.SpecFloat]
S754_nan [constructor, in Corelib.Floats.SpecFloat]
S754_infinity [constructor, in Corelib.Floats.SpecFloat]
S754_zero [constructor, in Corelib.Floats.SpecFloat]

---

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

(3486 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

(293 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

(51 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

(312 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

(100 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

(435 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

(611 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

(149 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

(99 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

(76 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

(117 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

(111 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

(108 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

(962 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

(62 entries)