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)

---

R

RedFlags [library]
Ref [library]
reflect [inductive, in Corelib.Init.Datatypes]
Reflect [section, in Corelib.ssr.ssrbool]
reflect [abbreviation, in Corelib.ssr.ssrbool]
ReflectCombinators [section, in Corelib.ssr.ssrbool]
ReflectCombinators.p [variable, in Corelib.ssr.ssrbool]
ReflectCombinators.P [variable, in Corelib.ssr.ssrbool]
ReflectCombinators.q [variable, in Corelib.ssr.ssrbool]
ReflectCombinators.Q [variable, in Corelib.ssr.ssrbool]
ReflectCombinators.rP [variable, in Corelib.ssr.ssrbool]
ReflectCombinators.rQ [variable, in Corelib.ssr.ssrbool]
ReflectConnectives [section, in Corelib.ssr.ssrbool]
ReflectConnectives.b1 [variable, in Corelib.ssr.ssrbool]
ReflectConnectives.b2 [variable, in Corelib.ssr.ssrbool]
ReflectConnectives.b3 [variable, in Corelib.ssr.ssrbool]
ReflectConnectives.b4 [variable, in Corelib.ssr.ssrbool]
ReflectConnectives.b5 [variable, in Corelib.ssr.ssrbool]
ReflectCore [section, in Corelib.ssr.ssrbool]
ReflectCore.b [variable, in Corelib.ssr.ssrbool]
ReflectCore.c [variable, in Corelib.ssr.ssrbool]
ReflectCore.Hb [variable, in Corelib.ssr.ssrbool]
ReflectCore.P [variable, in Corelib.ssr.ssrbool]
ReflectCore.Q [variable, in Corelib.ssr.ssrbool]
ReflectF [constructor, in Corelib.Init.Datatypes]
ReflectF [abbreviation, in Corelib.ssr.ssrbool]
ReflectNegCore [section, in Corelib.ssr.ssrbool]
ReflectNegCore.b [variable, in Corelib.ssr.ssrbool]
ReflectNegCore.c [variable, in Corelib.ssr.ssrbool]
ReflectNegCore.Hb [variable, in Corelib.ssr.ssrbool]
ReflectNegCore.P [variable, in Corelib.ssr.ssrbool]
ReflectNegCore.Q [variable, in Corelib.ssr.ssrbool]
ReflectT [constructor, in Corelib.Init.Datatypes]
ReflectT [abbreviation, in Corelib.ssr.ssrbool]
reflect_sind [definition, in Corelib.Init.Datatypes]
reflect_rec [definition, in Corelib.Init.Datatypes]
reflect_ind [definition, in Corelib.Init.Datatypes]
reflect_rect [definition, in Corelib.Init.Datatypes]
Reflect.b [variable, in Corelib.ssr.ssrbool]
Reflect.b' [variable, in Corelib.ssr.ssrbool]
Reflect.c [variable, in Corelib.ssr.ssrbool]
Reflect.P [variable, in Corelib.ssr.ssrbool]
Reflect.Pb [variable, in Corelib.ssr.ssrbool]
Reflect.Pb' [variable, in Corelib.ssr.ssrbool]
Reflect.Q [variable, in Corelib.ssr.ssrbool]
Reflexive [record, in Corelib.Classes.RelationClasses]
Reflexive [inductive, in Corelib.Classes.RelationClasses]
Reflexive [record, in Corelib.ssr.ssrclasses]
Reflexive [inductive, in Corelib.ssr.ssrclasses]
reflexive [definition, in Corelib.ssr.ssrbool]
Reflexive [record, in Corelib.Classes.CRelationClasses]
Reflexive [inductive, in Corelib.Classes.CRelationClasses]
reflexive [definition, in Corelib.Relations.Relation_Definitions]
ReflexiveProxy [record, in Corelib.Classes.Morphisms]
ReflexiveProxy [inductive, in Corelib.Classes.Morphisms]
reflexive_proper [lemma, in Corelib.Classes.CMorphisms]
Reflexive_partial_app_morphism [lemma, in Corelib.Classes.CMorphisms]
reflexive_eq_dom_reflexive [instance, in Corelib.Classes.CMorphisms]
reflexive_proper_proxy [lemma, in Corelib.Classes.CMorphisms]
Reflexive_partial_app_morphism [lemma, in Corelib.Classes.Morphisms]
reflexive_eq_dom_reflexive [instance, in Corelib.Classes.Morphisms]
reflexive_reflexive_proxy [lemma, in Corelib.Classes.Morphisms]
reflexive_proper_proxy [lemma, in Corelib.Classes.Morphisms]
reflexive_proper [lemma, in Corelib.Classes.Morphisms]
reflexive_proxy [projection, in Corelib.Classes.Morphisms]
reflexive_proxy [constructor, in Corelib.Classes.Morphisms]
reflexivity [projection, in Corelib.Classes.RelationClasses]
reflexivity [constructor, in Corelib.Classes.RelationClasses]
reflexivity [projection, in Corelib.ssr.ssrclasses]
reflexivity [constructor, in Corelib.ssr.ssrclasses]
reflexivity [projection, in Corelib.Classes.CRelationClasses]
reflexivity [constructor, in Corelib.Classes.CRelationClasses]
refl_id [abbreviation, in Corelib.Init.Datatypes]
refl_equal [abbreviation, in Corelib.Init.Logic]
registered_applicative_pred [record, in Corelib.ssr.ssrbool]
rel [definition, in Corelib.ssr.ssrbool]
relation [definition, in Corelib.Relations.Relation_Definitions]
RelationClasses [library]
RelationProperties [section, in Corelib.ssr.ssrbool]
RelationProperties.PER [section, in Corelib.ssr.ssrbool]
RelationProperties.PER.symR [variable, in Corelib.ssr.ssrbool]
RelationProperties.PER.trR [variable, in Corelib.ssr.ssrbool]
RelationProperties.R [variable, in Corelib.ssr.ssrbool]
RelationProperties.T [variable, in Corelib.ssr.ssrbool]
Relations [section, in Corelib.Classes.CMorphisms]
Relations [section, in Corelib.Classes.Morphisms]
Relations.A [variable, in Corelib.Classes.CMorphisms]
Relations.A [variable, in Corelib.Classes.Morphisms]
Relations.B [variable, in Corelib.Classes.Morphisms]
Relations.P [variable, in Corelib.Classes.Morphisms]
Relations.U [variable, in Corelib.Classes.Morphisms]
relation_implication_preorder [instance, in Corelib.Classes.RelationClasses]
relation_equivalence_equivalence [instance, in Corelib.Classes.RelationClasses]
relation_disjunction [definition, in Corelib.Classes.RelationClasses]
relation_conjunction [definition, in Corelib.Classes.RelationClasses]
relation_equivalence_rewrite_relation [instance, in Corelib.Classes.RelationClasses]
relation_equivalence [definition, in Corelib.Classes.RelationClasses]
relation_implication_preorder [instance, in Corelib.Classes.CRelationClasses]
relation_equivalence_equivalence [instance, in Corelib.Classes.CRelationClasses]
relation_disjunction [definition, in Corelib.Classes.CRelationClasses]
relation_conjunction [definition, in Corelib.Classes.CRelationClasses]
relation_equivalence [definition, in Corelib.Classes.CRelationClasses]
Relation_Definition.Relations_of_Relations [section, in Corelib.Relations.Relation_Definitions]
Relation_Definition.Sets_of_Relations [section, in Corelib.Relations.Relation_Definitions]
Relation_Definition.General_Properties_of_Relations [section, in Corelib.Relations.Relation_Definitions]
Relation_Definition.R [variable, in Corelib.Relations.Relation_Definitions]
Relation_Definition.A [variable, in Corelib.Relations.Relation_Definitions]
Relation_Definition [section, in Corelib.Relations.Relation_Definitions]
Relation_Definitions [library]
relpre [definition, in Corelib.ssr.ssrbool]
relU [definition, in Corelib.ssr.ssrbool]
rel_of_simpl [definition, in Corelib.ssr.ssrbool]
repeat [definition, in Corelib.Lists.ListDef]
Repeat [section, in Corelib.Lists.ListDef]
Repeat.A [variable, in Corelib.Lists.ListDef]
respectful [definition, in Corelib.Classes.CMorphisms]
respectful [definition, in Corelib.Classes.Morphisms]
respectful_morphism [instance, in Corelib.Classes.CMorphisms]
respectful_per [instance, in Corelib.Classes.CMorphisms]
respectful_hetero [definition, in Corelib.Classes.CMorphisms]
respectful_morphism [instance, in Corelib.Classes.Morphisms]
respectful_per [instance, in Corelib.Classes.Morphisms]
respectful_hetero [definition, in Corelib.Classes.Morphisms]
respecting [definition, in Corelib.Classes.Equivalence]
Respecting [section, in Corelib.Classes.Equivalence]
respecting_equiv [instance, in Corelib.Classes.Equivalence]
returnType [definition, in Corelib.ssr.ssreflect]
rev [definition, in Corelib.Init.Hexadecimal]
rev [definition, in Corelib.Init.Decimal]
revapp [definition, in Corelib.Init.Hexadecimal]
revapp [definition, in Corelib.Init.Decimal]
ReverseCoercionSource [definition, in Corelib.Init.Prelude]
ReverseCoercionTarget [definition, in Corelib.Init.Prelude]
reverse_coercion [definition, in Corelib.Init.Prelude]
rev_trans [lemma, in Corelib.ssr.ssrbool]
rev_left_loop [definition, in Corelib.ssr.ssrfun]
rev_right_loop [definition, in Corelib.ssr.ssrfun]
RewriteRelation [record, in Corelib.Classes.RelationClasses]
RewriteRelation [record, in Corelib.Classes.CRelationClasses]
rewrite_relation_eq_dom [lemma, in Corelib.Classes.Morphisms]
rewrite_relation_pointwise [lemma, in Corelib.Classes.Morphisms]
rew_pair [lemma, in Corelib.Init.Datatypes]
rew_sig2 [lemma, in Corelib.Init.Specif]
rew_sigT2 [lemma, in Corelib.Init.Specif]
rew_sig [lemma, in Corelib.Init.Specif]
rew_sigT [lemma, in Corelib.Init.Specif]
rew_ex2 [lemma, in Corelib.Init.Logic]
rew_ex [lemma, in Corelib.Init.Logic]
rew_const [lemma, in Corelib.Init.Logic]
rew_compose [lemma, in Corelib.Init.Logic]
rew_swap [lemma, in Corelib.Init.Logic]
rew_map [lemma, in Corelib.Init.Logic]
rew_opp_l [lemma, in Corelib.Init.Logic]
rew_opp_r [lemma, in Corelib.Init.Logic]
right [constructor, in Corelib.Init.Specif]
right_transitive [definition, in Corelib.ssr.ssrbool]
right_distributive [definition, in Corelib.ssr.ssrfun]
right_zero [definition, in Corelib.ssr.ssrfun]
right_loop [definition, in Corelib.ssr.ssrfun]
right_commutative [definition, in Corelib.ssr.ssrfun]
right_id [definition, in Corelib.ssr.ssrfun]
right_injective [definition, in Corelib.ssr.ssrfun]
right_inverse [definition, in Corelib.ssr.ssrfun]
RocqGenericDependentIf [abbreviation, in Corelib.ssr.ssreflect]
RocqGenericIf [abbreviation, in Corelib.ssr.ssreflect]
round_nearest_even [definition, in Corelib.Floats.SpecFloat]
rrefl [lemma, in Corelib.ssr.ssrfun]
rwP [lemma, in Corelib.ssr.ssrbool]
rwP2 [lemma, in Corelib.ssr.ssrbool]

---

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)