Rocq Core Library

Global Index

J

Y

_

(3486 entries)

Notation Index

A

B

C

D

F

G

H

J

K

L

M

N

O

Q

R

T

V

W

X

Y

_

(293 entries)

Module Index

A

G

H

J

K

M

Q

R

V

W

X

Y

_

other

(51 entries)

Variable Index

J

Q

V

X

Y

Z

_

other

(312 entries)

Library Index

G

J

K

Q

V

X

Y

Z

_

other

(100 entries)

Constructor Index

J

K

W

Y

_

other

(435 entries)

Lemma Index

J

V

Y

Z

_

other

(611 entries)

Axiom Index

B

J

K

Q

R

V

W

X

Y

Z

_

other

(149 entries)

Inductive Index

G

J

K

W

X

Y

_

other

(99 entries)

Projection Index

B

D

G

H

J

K

L

Q

W

X

Y

Z

_

other

(76 entries)

Instance Index

B

D

G

H

J

K

L

M

Q

U

V

X

Y

Z

_

other

(117 entries)

Section Index

J

Q

V

X

Y

Z

_

other

(111 entries)

Abbreviation Index

B

G

H

J

K

L

Q

W

Y

_

other

(108 entries)

Definition Index

J

Q

Y

_

other

(962 entries)

Record Index

B

G

H

J

L

Q

X

Y

Z

_

other

(62 entries)

other (notation)

if _ as _ return _ then _ else _ (boolean_if_scope) [in Corelib.ssr.ssreflect]
if _ then _ else _ (boolean_if_scope) [in Corelib.ssr.ssreflect]
if _ return _ then _ else _ (boolean_if_scope) [in Corelib.ssr.ssreflect]
_ && _ (bool_scope) [in Corelib.Init.Datatypes]
_ || _ (bool_scope) [in Corelib.Init.Datatypes]
_ \is an _ (bool_scope) [in Corelib.ssr.ssrbool]
_ \is a _ (bool_scope) [in Corelib.ssr.ssrbool]
_ \is _ (bool_scope) [in Corelib.ssr.ssrbool]
_ \in _ (bool_scope) [in Corelib.ssr.ssrbool]
_ \isn't an _ (bool_scope) [in Corelib.ssr.ssrbool]
_ \isn't a _ (bool_scope) [in Corelib.ssr.ssrbool]
_ \isn't _ (bool_scope) [in Corelib.ssr.ssrbool]
_ \is an _ (bool_scope) [in Corelib.ssr.ssrbool]
_ \is an _ (bool_scope) [in Corelib.ssr.ssrbool]
_ \is a _ (bool_scope) [in Corelib.ssr.ssrbool]
_ \is a _ (bool_scope) [in Corelib.ssr.ssrbool]
_ \is _ (bool_scope) [in Corelib.ssr.ssrbool]
_ \is _ (bool_scope) [in Corelib.ssr.ssrbool]
_ \notin _ (bool_scope) [in Corelib.ssr.ssrbool]
_ \in _ (bool_scope) [in Corelib.ssr.ssrbool]
_ \in _ (bool_scope) [in Corelib.ssr.ssrbool]
[ ==> _ => _ ] (bool_scope) [in Corelib.ssr.ssrbool]
[ ==> _ , _ , .. , _ => _ ] (bool_scope) [in Corelib.ssr.ssrbool]
[ || _ , _ , .. , _ | _ ] (bool_scope) [in Corelib.ssr.ssrbool]
[ || _ | _ ] (bool_scope) [in Corelib.ssr.ssrbool]
[ && _ , _ , .. , _ & _ ] (bool_scope) [in Corelib.ssr.ssrbool]
[ && _ & _ ] (bool_scope) [in Corelib.ssr.ssrbool]
_ (+) _ (bool_scope) [in Corelib.ssr.ssrbool]
_ ==> _ (bool_scope) [in Corelib.ssr.ssrbool]
~~ _ (bool_scope) [in Corelib.ssr.ssrbool]
( _ , _ , .. , _ ) (core_scope) [in Corelib.Init.Datatypes]
_ =~= _ (equiv_scope) [in Corelib.Classes.Equivalence]
_ =/= _ (equiv_scope) [in Corelib.Classes.Equivalence]
_ === _ (equiv_scope) [in Corelib.Classes.Equivalence]
[ qualify an _ : _ | _ ] (form_scope) [in Corelib.ssr.ssrbool]
[ qualify an _ | _ ] (form_scope) [in Corelib.ssr.ssrbool]
[ qualify a _ : _ | _ ] (form_scope) [in Corelib.ssr.ssrbool]
[ qualify a _ | _ ] (form_scope) [in Corelib.ssr.ssrbool]
[ qualify _ : _ | _ ] (form_scope) [in Corelib.ssr.ssrbool]
[ qualify _ | _ ] (form_scope) [in Corelib.ssr.ssrbool]
[ predType of _ ] (form_scope) [in Corelib.ssr.ssrbool]
[ unlockable fun _ ] (form_scope) [in Corelib.ssr.ssreflect]
[ unlockable of _ ] (form_scope) [in Corelib.ssr.ssreflect]
=^~ _ (form_scope) [in Corelib.ssr.ssreflect]
[ the _ of _ ] (form_scope) [in Corelib.ssr.ssreflect]
[ the _ of _ by _ ] (form_scope) [in Corelib.ssr.ssreflect]
[ the _ of _ ] (form_scope) [in Corelib.ssr.ssreflect]
[ the _ of _ by _ ] (form_scope) [in Corelib.ssr.ssreflect]
[ rel _ _ in _ ] (function_scope) [in Corelib.ssr.ssrbool]
[ rel _ _ in _ | _ ] (function_scope) [in Corelib.ssr.ssrbool]
[ rel _ _ in _ & _ ] (function_scope) [in Corelib.ssr.ssrbool]
[ rel _ _ in _ & _ | _ ] (function_scope) [in Corelib.ssr.ssrbool]
[ pred _ in _ | _ & _ ] (function_scope) [in Corelib.ssr.ssrbool]
[ pred _ in _ | _ ] (function_scope) [in Corelib.ssr.ssrbool]
[ pred _ in _ ] (function_scope) [in Corelib.ssr.ssrbool]
[ preim _ of _ ] (function_scope) [in Corelib.ssr.ssrbool]
[ predC _ ] (function_scope) [in Corelib.ssr.ssrbool]
[ predD _ & _ ] (function_scope) [in Corelib.ssr.ssrbool]
[ predU _ & _ ] (function_scope) [in Corelib.ssr.ssrbool]
[ predI _ & _ ] (function_scope) [in Corelib.ssr.ssrbool]
[ mem _ ] (function_scope) [in Corelib.ssr.ssrbool]
[ in _ ] (function_scope) [in Corelib.ssr.ssrbool]
[ rel _ _ : _ | _ ] (function_scope) [in Corelib.ssr.ssrbool]
[ rel _ _ | _ ] (function_scope) [in Corelib.ssr.ssrbool]
[ pred _ : _ | _ & _ ] (function_scope) [in Corelib.ssr.ssrbool]
[ pred _ : _ | _ ] (function_scope) [in Corelib.ssr.ssrbool]
[ pred _ | _ & _ ] (function_scope) [in Corelib.ssr.ssrbool]
[ pred _ | _ ] (function_scope) [in Corelib.ssr.ssrbool]
[ pred : _ | _ ] (function_scope) [in Corelib.ssr.ssrbool]
@ sval (function_scope) [in Corelib.ssr.ssrfun]
@ id _ (function_scope) [in Corelib.ssr.ssrfun]
fun => _ (function_scope) [in Corelib.ssr.ssrfun]
[ eta _ ] (function_scope) [in Corelib.ssr.ssrfun]
_ \; _ (function_scope) [in Corelib.ssr.ssrfun]
_ \o _ (function_scope) [in Corelib.ssr.ssrfun]
[ fun ( _ : _ ) ( _ : _ ) => _ ] (function_scope) [in Corelib.ssr.ssrfun]
[ fun _ ( _ : _ ) => _ ] (function_scope) [in Corelib.ssr.ssrfun]
[ fun ( _ : _ ) _ => _ ] (function_scope) [in Corelib.ssr.ssrfun]
[ fun _ _ : _ => _ ] (function_scope) [in Corelib.ssr.ssrfun]
[ fun _ : _ => _ ] (function_scope) [in Corelib.ssr.ssrfun]
[ fun _ _ => _ ] (function_scope) [in Corelib.ssr.ssrfun]
[ fun _ => _ ] (function_scope) [in Corelib.ssr.ssrfun]
[ fun : _ => _ ] (function_scope) [in Corelib.ssr.ssrfun]
@^~ _ (function_scope) [in Corelib.ssr.ssrfun]
_ ^~ _ (function_scope) [in Corelib.ssr.ssrfun]
if _ as _ return _ then _ else _ (general_if_scope) [in Corelib.ssr.ssreflect]
if _ return _ then _ else _ (general_if_scope) [in Corelib.ssr.ssreflect]
if _ then _ else _ (general_if_scope) [in Corelib.ssr.ssreflect]
_ ++ _ (list_scope) [in Corelib.Init.Datatypes]
_ :: _ (list_scope) [in Corelib.Init.Datatypes]
_ mod _ (nat_scope) [in Corelib.Init.Nat]
_ / _ (nat_scope) [in Corelib.Init.Nat]
_ ^ _ (nat_scope) [in Corelib.Init.Nat]
_ ?= _ (nat_scope) [in Corelib.Init.Nat]
_ <? _ (nat_scope) [in Corelib.Init.Nat]
_ <=? _ (nat_scope) [in Corelib.Init.Nat]
_ =? _ (nat_scope) [in Corelib.Init.Nat]
_ - _ (nat_scope) [in Corelib.Init.Nat]
_ * _ (nat_scope) [in Corelib.Init.Nat]
_ + _ (nat_scope) [in Corelib.Init.Nat]
_ < _ <= _ (nat_scope) [in Corelib.Init.Peano]
_ < _ < _ (nat_scope) [in Corelib.Init.Peano]
_ <= _ < _ (nat_scope) [in Corelib.Init.Peano]
_ <= _ <= _ (nat_scope) [in Corelib.Init.Peano]
_ > _ (nat_scope) [in Corelib.Init.Peano]
_ >= _ (nat_scope) [in Corelib.Init.Peano]
_ < _ (nat_scope) [in Corelib.Init.Peano]
_ <= _ (nat_scope) [in Corelib.Init.Peano]
_ - _ (nat_scope) [in Corelib.Init.Peano]
_ * _ (nat_scope) [in Corelib.Init.Peano]
_ + _ (nat_scope) [in Corelib.Init.Peano]
_ .2 (pair_scope) [in Corelib.ssr.ssrfun]
_ .1 (pair_scope) [in Corelib.ssr.ssrfun]
3 (positive_scope) [in Corelib.BinNums.PosDef]
2 (positive_scope) [in Corelib.BinNums.PosDef]
1 (positive_scope) [in Corelib.BinNums.PosDef]
_ ~ 0 (positive_scope) [in Corelib.BinNums.PosDef]
_ ~ 1 (positive_scope) [in Corelib.BinNums.PosDef]
∙⊥∙ (predicate_scope) [in Corelib.Classes.RelationClasses]
∙⊤∙ (predicate_scope) [in Corelib.Classes.RelationClasses]
_ \∙/ _ (predicate_scope) [in Corelib.Classes.RelationClasses]
_ /∙\ _ (predicate_scope) [in Corelib.Classes.RelationClasses]
_ -∙> _ (predicate_scope) [in Corelib.Classes.RelationClasses]
_ <∙> _ (predicate_scope) [in Corelib.Classes.RelationClasses]
_ ∘ _ (program_scope) [in Corelib.Program.Basics]
` _ (program_scope) [in Corelib.Program.Utils]
! (program_scope) [in Corelib.Program.Utils]
_ (* _ *) (ssr_scope) [in Corelib.ssr.ssreflect]
<hidden _ > (ssr_scope) [in Corelib.ssr.ssreflect]
_ * _ (type_scope) [in Corelib.Init.Datatypes]
_ + _ (type_scope) [in Corelib.Init.Datatypes]
{ on _ , bijective _ } (type_scope) [in Corelib.ssr.ssrbool]
{ in _ , bijective _ } (type_scope) [in Corelib.ssr.ssrbool]
{ on _ , _ & _ } (type_scope) [in Corelib.ssr.ssrbool]
{ on _ & , _ } (type_scope) [in Corelib.ssr.ssrbool]
{ on _ , _ } (type_scope) [in Corelib.ssr.ssrbool]
{ in _ & & , _ } (type_scope) [in Corelib.ssr.ssrbool]
{ in _ & _ & , _ } (type_scope) [in Corelib.ssr.ssrbool]
{ in _ & & _ , _ } (type_scope) [in Corelib.ssr.ssrbool]
{ in _ & _ & _ , _ } (type_scope) [in Corelib.ssr.ssrbool]
{ in _ & , _ } (type_scope) [in Corelib.ssr.ssrbool]
{ in _ & _ , _ } (type_scope) [in Corelib.ssr.ssrbool]
{ in _ , _ } (type_scope) [in Corelib.ssr.ssrbool]
{ for _ , _ } (type_scope) [in Corelib.ssr.ssrbool]
{ subset _ <= _ } (type_scope) [in Corelib.ssr.ssrbool]
_ =i _ (type_scope) [in Corelib.ssr.ssrbool]
{ : _ } (type_scope) [in Corelib.ssr.ssrbool]
{ pred _ } (type_scope) [in Corelib.ssr.ssrbool]
[ \/ _ , _ , _ | _ ] (type_scope) [in Corelib.ssr.ssrbool]
[ \/ _ , _ | _ ] (type_scope) [in Corelib.ssr.ssrbool]
[ \/ _ | _ ] (type_scope) [in Corelib.ssr.ssrbool]
[ /\ _ , _ , _ , _ & _ ] (type_scope) [in Corelib.ssr.ssrbool]
[ /\ _ , _ , _ & _ ] (type_scope) [in Corelib.ssr.ssrbool]
[ /\ _ , _ & _ ] (type_scope) [in Corelib.ssr.ssrbool]
[ /\ _ & _ ] (type_scope) [in Corelib.ssr.ssrbool]
\unless _ , _ (type_scope) [in Corelib.ssr.ssrbool]
{ type of _ for _ } (type_scope) [in Corelib.ssr.ssreflect]
_ + { _ } (type_scope) [in Corelib.Init.Specif]
{ _ } + { _ } (type_scope) [in Corelib.Init.Specif]
{ ' _ : _ & _ & _ } (type_scope) [in Corelib.Init.Specif]
{ ' _ : _ & _ } (type_scope) [in Corelib.Init.Specif]
{ ' _ & _ & _ } (type_scope) [in Corelib.Init.Specif]
{ ' _ & _ } (type_scope) [in Corelib.Init.Specif]
{ ' _ : _ | _ & _ } (type_scope) [in Corelib.Init.Specif]
{ ' _ : _ | _ } (type_scope) [in Corelib.Init.Specif]
{ ' _ | _ & _ } (type_scope) [in Corelib.Init.Specif]
{ ' _ | _ } (type_scope) [in Corelib.Init.Specif]
{ _ : _ & _ & _ } (type_scope) [in Corelib.Init.Specif]
{ _ : _ & _ } (type_scope) [in Corelib.Init.Specif]
{ _ & _ & _ } (type_scope) [in Corelib.Init.Specif]
{ _ & _ } (type_scope) [in Corelib.Init.Specif]
{ _ : _ | _ & _ } (type_scope) [in Corelib.Init.Specif]
{ _ : _ | _ } (type_scope) [in Corelib.Init.Specif]
{ _ | _ & _ } (type_scope) [in Corelib.Init.Specif]
{ _ | _ } (type_scope) [in Corelib.Init.Specif]
{ mono _ : _ _ /~ _ } (type_scope) [in Corelib.ssr.ssrfun]
{ mono _ : _ _ / _ } (type_scope) [in Corelib.ssr.ssrfun]
{ mono _ : _ _ / _ >-> _ } (type_scope) [in Corelib.ssr.ssrfun]
{ mono _ : _ / _ } (type_scope) [in Corelib.ssr.ssrfun]
{ mono _ : _ / _ >-> _ } (type_scope) [in Corelib.ssr.ssrfun]
{ homo _ : _ _ /~ _ } (type_scope) [in Corelib.ssr.ssrfun]
{ homo _ : _ _ / _ } (type_scope) [in Corelib.ssr.ssrfun]
{ homo _ : _ _ / _ >-> _ } (type_scope) [in Corelib.ssr.ssrfun]
{ homo _ : _ / _ } (type_scope) [in Corelib.ssr.ssrfun]
{ homo _ : _ / _ >-> _ } (type_scope) [in Corelib.ssr.ssrfun]
{ morph _ : _ _ / _ } (type_scope) [in Corelib.ssr.ssrfun]
{ morph _ : _ _ / _ >-> _ } (type_scope) [in Corelib.ssr.ssrfun]
{ morph _ : _ / _ } (type_scope) [in Corelib.ssr.ssrfun]
{ morph _ : _ / _ >-> _ } (type_scope) [in Corelib.ssr.ssrfun]
_ =2 _ :> _ (type_scope) [in Corelib.ssr.ssrfun]
_ =2 _ (type_scope) [in Corelib.ssr.ssrfun]
_ =1 _ :> _ (type_scope) [in Corelib.ssr.ssrfun]
_ =1 _ (type_scope) [in Corelib.ssr.ssrfun]
exists ! _ .. _ , _ (type_scope) [in Corelib.Init.Logic]
_ <> _ (type_scope) [in Corelib.Init.Logic]
_ <> _ :> _ (type_scope) [in Corelib.Init.Logic]
_ = _ (type_scope) [in Corelib.Init.Logic]
_ = _ :> _ (type_scope) [in Corelib.Init.Logic]
exists2 ' _ : _ , _ & _ (type_scope) [in Corelib.Init.Logic]
exists2 ' _ , _ & _ (type_scope) [in Corelib.Init.Logic]
exists2 _ : _ , _ & _ (type_scope) [in Corelib.Init.Logic]
exists2 _ , _ & _ (type_scope) [in Corelib.Init.Logic]
exists _ .. _ , _ (type_scope) [in Corelib.Init.Logic]
_ <-> _ (type_scope) [in Corelib.Init.Logic]
_ \/ _ (type_scope) [in Corelib.Init.Logic]
_ /\ _ (type_scope) [in Corelib.Init.Logic]
~ _ (type_scope) [in Corelib.Init.Logic]
_ -> _ (type_scope) [in Corelib.Init.Logic]
{ ( _ , _ ) : _ | _ } (type_scope) [in Corelib.Program.Utils]
_ <= _ < _ (Z_scope) [in Corelib.Numbers.Cyclic.Int63.Uint63Axioms]
_ < _ (Z_scope) [in Corelib.Numbers.Cyclic.Int63.Uint63Axioms]
_ <= _ (Z_scope) [in Corelib.Numbers.Cyclic.Int63.Uint63Axioms]
_ ^ _ (Z_scope) [in Corelib.Numbers.Cyclic.Int63.Uint63Axioms]
_ * _ (Z_scope) [in Corelib.Numbers.Cyclic.Int63.Uint63Axioms]
_ - _ (Z_scope) [in Corelib.Numbers.Cyclic.Int63.Uint63Axioms]
_ + _ (Z_scope) [in Corelib.Numbers.Cyclic.Int63.Uint63Axioms]
2 (Z_scope) [in Corelib.Numbers.Cyclic.Int63.Uint63Axioms]
1 (Z_scope) [in Corelib.Numbers.Cyclic.Int63.Uint63Axioms]
0 (Z_scope) [in Corelib.Numbers.Cyclic.Int63.Uint63Axioms]
_ < _ (Z_scope) [in Corelib.Numbers.Cyclic.Int63.Sint63Axioms]
_ <= _ (Z_scope) [in Corelib.Numbers.Cyclic.Int63.Sint63Axioms]
_ ^ _ (Z_scope) [in Corelib.Numbers.Cyclic.Int63.Sint63Axioms]
2 (Z_scope) [in Corelib.Numbers.Cyclic.Int63.Sint63Axioms]
_ :: _ [in Corelib.Classes.RelationClasses]
_ .3 [in Corelib.Init.Specif]
0 [in Corelib.BinNums.IntDef]
0 [in Corelib.Init.Byte]
0 [in Corelib.Init.Nat]
0 [in Corelib.Init.Peano]
1 [in Corelib.BinNums.IntDef]
1 [in Corelib.Init.Byte]
1 [in Corelib.Init.Nat]
2 [in Corelib.BinNums.IntDef]
2 [in Corelib.Init.Nat]
[ elaborate _ ] [in Corelib.ssr.ssreflect]
{ all3 _ } [in Corelib.ssr.ssrbool]
{ all2 _ } [in Corelib.ssr.ssrbool]
{ all1 _ } [in Corelib.ssr.ssrbool]

Global Index

J

Y

_

(3486 entries)

Notation Index

A

B

C

D

F

G

H

J

K

L

M

N

O

Q

R

T

V

W

X

Y

_

(293 entries)

Module Index

A

G

H

J

K

M

Q

R

V

W

X

Y

_

other

(51 entries)

Variable Index

J

Q

V

X

Y

Z

_

other

(312 entries)

Library Index

G

J

K

Q

V

X

Y

Z

_

other

(100 entries)

Constructor Index

J

K

W

Y

_

other

(435 entries)

Lemma Index

J

V

Y

Z

_

other

(611 entries)

Axiom Index

B

J

K

Q

R

V

W

X

Y

Z

_

other

(149 entries)

Inductive Index

G

J

K

W

X

Y

_

other

(99 entries)

Projection Index

B

D

G

H

J

K

L

Q

W

X

Y

Z

_

other

(76 entries)

Instance Index

B

D

G

H

J

K

L

M

Q

U

V

X

Y

Z

_

other

(117 entries)

Section Index

J

Q

V

X

Y

Z

_

other

(111 entries)

Abbreviation Index

B

G

H

J

K

L

Q

W

Y

_

other

(108 entries)

Definition Index

J

Q

Y

_

other

(962 entries)

Record Index

B

G

H

J

L

Q

X

Y

Z

_

other

(62 entries)