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)

I

I [constructor, in Corelib.Init.Logic]
id [definition, in Corelib.Init.Datatypes]
ID [definition, in Corelib.Init.Datatypes]
id [abbreviation, in Corelib.ssr.ssrfun]
idempotent [definition, in Corelib.ssr.ssrfun]
Ident [library]
identity [abbreviation, in Corelib.Init.Datatypes]
identity_rect_r [abbreviation, in Corelib.Init.Datatypes]
identity_rec_r [abbreviation, in Corelib.Init.Datatypes]
identity_ind_r [abbreviation, in Corelib.Init.Datatypes]
identity_congr [abbreviation, in Corelib.Init.Datatypes]
identity_trans [abbreviation, in Corelib.Init.Datatypes]
identity_sym [abbreviation, in Corelib.Init.Datatypes]
identity_rect [abbreviation, in Corelib.Init.Datatypes]
identity_rec [abbreviation, in Corelib.Init.Datatypes]
identity_ind [abbreviation, in Corelib.Init.Datatypes]
identity_refl [abbreviation, in Corelib.Init.Datatypes]
idfun [definition, in Corelib.ssr.ssrfun]
idP [lemma, in Corelib.ssr.ssrbool]
idPn [lemma, in Corelib.ssr.ssrbool]
idProp [definition, in Corelib.Init.Datatypes]
IDProp [definition, in Corelib.Init.Datatypes]
id_int [definition, in Corelib.Numbers.Cyclic.Int63.PrimInt63]
ifE [lemma, in Corelib.ssr.ssrbool]
ifF [lemma, in Corelib.ssr.ssrbool]
iff [definition, in Corelib.Init.Logic]
iffLR [lemma, in Corelib.ssr.ssreflect]
iffLRn [lemma, in Corelib.ssr.ssreflect]
iffP [lemma, in Corelib.ssr.ssrbool]
iffRL [lemma, in Corelib.ssr.ssreflect]
iffRLn [lemma, in Corelib.ssr.ssreflect]
iffT [definition, in Corelib.Classes.CRelationClasses]
iffT_flip_arrow_subrelation [instance, in Corelib.Classes.CMorphisms]
iffT_arrow_subrelation [instance, in Corelib.Classes.CMorphisms]
iffT_Transitive [instance, in Corelib.Classes.CRelationClasses]
iffT_Symmetric [instance, in Corelib.Classes.CRelationClasses]
iffT_Reflexive [instance, in Corelib.Classes.CRelationClasses]
iff_equivalence [instance, in Corelib.Classes.RelationClasses]
iff_Transitive [instance, in Corelib.Classes.RelationClasses]
iff_Symmetric [instance, in Corelib.Classes.RelationClasses]
iff_Reflexive [instance, in Corelib.Classes.RelationClasses]
iff_rewrite_relation [instance, in Corelib.Classes.RelationClasses]
iff_Reflexive [instance, in Corelib.ssr.ssrclasses]
iff_flip_impl_subrelation [instance, in Corelib.Classes.CMorphisms]
iff_impl_subrelation [instance, in Corelib.Classes.CMorphisms]
iff_pars [instance, in Corelib.Classes.Morphisms]
iff_flip_impl_subrelation [instance, in Corelib.Classes.Morphisms]
iff_impl_subrelation [instance, in Corelib.Classes.Morphisms]
iff_equivalence [instance, in Corelib.Classes.CRelationClasses]
iff_Transitive [instance, in Corelib.Classes.CRelationClasses]
iff_Symmetric [instance, in Corelib.Classes.CRelationClasses]
iff_Reflexive [instance, in Corelib.Classes.CRelationClasses]
iff_stepl [lemma, in Corelib.Init.Logic]
iff_to_and [lemma, in Corelib.Init.Logic]
iff_and [lemma, in Corelib.Init.Logic]
iff_sym [lemma, in Corelib.Init.Logic]
iff_trans [lemma, in Corelib.Init.Logic]
iff_refl [lemma, in Corelib.Init.Logic]
iff_iff_iff_impl_morphism [instance, in Corelib.Classes.Morphisms_Prop]
ifN [lemma, in Corelib.ssr.ssrbool]
IfNotations [module, in Corelib.Init.Notations]
if _ is _ then _ else _ [notation, in Corelib.Init.Notations]
ifP [lemma, in Corelib.ssr.ssrbool]
ifPn [lemma, in Corelib.ssr.ssrbool]
IfSpecFalse [constructor, in Corelib.ssr.ssrbool]
IfSpecTrue [constructor, in Corelib.ssr.ssrbool]
ifT [lemma, in Corelib.ssr.ssrbool]
if_expr [definition, in Corelib.ssr.ssrbool]
if_arg [lemma, in Corelib.ssr.ssrbool]
if_neg [lemma, in Corelib.ssr.ssrbool]
if_same [lemma, in Corelib.ssr.ssrbool]
if_spec [inductive, in Corelib.ssr.ssrbool]
impl [definition, in Corelib.Program.Basics]
implb [definition, in Corelib.Init.Datatypes]
Implies [constructor, in Corelib.ssr.ssrbool]
implies [inductive, in Corelib.ssr.ssrbool]
impliesP [lemma, in Corelib.ssr.ssrbool]
impliesPn [lemma, in Corelib.ssr.ssrbool]
implybb [lemma, in Corelib.ssr.ssrbool]
implybE [lemma, in Corelib.ssr.ssrbool]
implybF [lemma, in Corelib.ssr.ssrbool]
implybN [lemma, in Corelib.ssr.ssrbool]
implybNN [lemma, in Corelib.ssr.ssrbool]
implybT [lemma, in Corelib.ssr.ssrbool]
implyb_id2l [lemma, in Corelib.ssr.ssrbool]
implyb_idr [lemma, in Corelib.ssr.ssrbool]
implyb_idl [lemma, in Corelib.ssr.ssrbool]
implyFb [lemma, in Corelib.ssr.ssrbool]
implyNb [lemma, in Corelib.ssr.ssrbool]
implyP [lemma, in Corelib.ssr.ssrbool]
implyPP [lemma, in Corelib.ssr.ssrbool]
implyTb [lemma, in Corelib.ssr.ssrbool]
impl_Transitive [instance, in Corelib.Classes.RelationClasses]
impl_Reflexive [instance, in Corelib.Classes.RelationClasses]
impl_rewrite_relation [instance, in Corelib.Classes.RelationClasses]
impl_pars [instance, in Corelib.Classes.Morphisms]
impl_Transitive [instance, in Corelib.Classes.CRelationClasses]
impl_Reflexive [instance, in Corelib.Classes.CRelationClasses]
imp_iff_compat_r [lemma, in Corelib.Init.Logic]
imp_iff_compat_l [lemma, in Corelib.Init.Logic]
inclusion [definition, in Corelib.Relations.Relation_Definitions]
Ind [library]
inE [definition, in Corelib.ssr.ssrbool]
infinity [definition, in Corelib.Floats.PrimFloat]
inhabited [inductive, in Corelib.Init.Logic]
inhabited_sig_to_exists [lemma, in Corelib.Init.Specif]
inhabited_covariant [lemma, in Corelib.Init.Logic]
inhabited_sind [definition, in Corelib.Init.Logic]
inhabited_ind [definition, in Corelib.Init.Logic]
inhabits [constructor, in Corelib.Init.Logic]
Init [library]
Init [library]
Injections [section, in Corelib.ssr.ssrfun]
InjectionsTheory [section, in Corelib.ssr.ssrfun]
InjectionsTheory.A [variable, in Corelib.ssr.ssrfun]
InjectionsTheory.B [variable, in Corelib.ssr.ssrfun]
InjectionsTheory.C [variable, in Corelib.ssr.ssrfun]
InjectionsTheory.f [variable, in Corelib.ssr.ssrfun]
InjectionsTheory.g [variable, in Corelib.ssr.ssrfun]
InjectionsTheory.h [variable, in Corelib.ssr.ssrfun]
Injections.aT [variable, in Corelib.ssr.ssrfun]
Injections.f [variable, in Corelib.ssr.ssrfun]
Injections.rT [variable, in Corelib.ssr.ssrfun]
injective [definition, in Corelib.ssr.ssrfun]
injective_projections [lemma, in Corelib.Init.Datatypes]
inj_can_sym_in [lemma, in Corelib.ssr.ssrbool]
inj_can_sym_on [lemma, in Corelib.ssr.ssrbool]
inj_can_sym_in_on [lemma, in Corelib.ssr.ssrbool]
inj_can_sym_in_on.g [variable, in Corelib.ssr.ssrbool]
inj_can_sym_in_on.f [variable, in Corelib.ssr.ssrbool]
inj_can_sym_in_on.rD [variable, in Corelib.ssr.ssrbool]
inj_can_sym_in_on.aD [variable, in Corelib.ssr.ssrbool]
inj_can_sym_in_on.rT [variable, in Corelib.ssr.ssrbool]
inj_can_sym_in_on.aT [variable, in Corelib.ssr.ssrbool]
inj_can_sym_in_on [section, in Corelib.ssr.ssrbool]
inj_can_eq [lemma, in Corelib.ssr.ssrfun]
inj_compr [lemma, in Corelib.ssr.ssrfun]
inj_comp [lemma, in Corelib.ssr.ssrfun]
inj_can_sym [lemma, in Corelib.ssr.ssrfun]
inj_id [lemma, in Corelib.ssr.ssrfun]
inl [constructor, in Corelib.Init.Datatypes]
inleft [constructor, in Corelib.Init.Specif]
inPhantom [definition, in Corelib.ssr.ssrbool]
inr [constructor, in Corelib.Init.Datatypes]
inright [constructor, in Corelib.Init.Specif]
inst [lemma, in Corelib.Init.Logic]
int [abbreviation, in Corelib.Init.Hexadecimal]
int [abbreviation, in Corelib.Init.Decimal]
int [abbreviation, in Corelib.Init.Number]
int [axiom, in Corelib.Numbers.Cyclic.Int63.PrimInt63]
Int [library]
IntDecimal [constructor, in Corelib.Init.Number]
IntDef [library]
interchange [definition, in Corelib.ssr.ssrfun]
internal_int_dec_bl [abbreviation, in Corelib.Init.Hexadecimal]
internal_int_dec_lb [abbreviation, in Corelib.Init.Hexadecimal]
internal_int_dec_bl [abbreviation, in Corelib.Init.Decimal]
internal_int_dec_lb [abbreviation, in Corelib.Init.Decimal]
internal_int_dec_bl [abbreviation, in Corelib.Init.Number]
internal_int_dec_lb [abbreviation, in Corelib.Init.Number]
IntHexadecimal [constructor, in Corelib.Init.Number]
introF [lemma, in Corelib.ssr.ssrbool]
introFn [lemma, in Corelib.ssr.ssrbool]
introN [lemma, in Corelib.ssr.ssrbool]
introNf [lemma, in Corelib.ssr.ssrbool]
introNTF [lemma, in Corelib.ssr.ssrbool]
introP [lemma, in Corelib.ssr.ssrbool]
introT [lemma, in Corelib.ssr.ssrbool]
introTF [lemma, in Corelib.ssr.ssrbool]
introTFn [lemma, in Corelib.ssr.ssrbool]
introTn [lemma, in Corelib.ssr.ssrbool]
inT_bij [lemma, in Corelib.ssr.ssrbool]
int_beq [abbreviation, in Corelib.Init.Hexadecimal]
int_eq_dec [abbreviation, in Corelib.Init.Hexadecimal]
int_of_int [definition, in Corelib.Init.Decimal]
int_beq [abbreviation, in Corelib.Init.Decimal]
int_eq_dec [abbreviation, in Corelib.Init.Decimal]
int_of_int [definition, in Corelib.Init.Number]
int_beq [abbreviation, in Corelib.Init.Number]
int_eq_dec [abbreviation, in Corelib.Init.Number]
int_wrap [projection, in Corelib.Numbers.Cyclic.Int63.PrimInt63]
int_wrapper [record, in Corelib.Numbers.Cyclic.Int63.PrimInt63]
Int63NotationsInternalA [module, in Corelib.Numbers.Cyclic.Int63.PrimInt63]
inverse_impl_rewrite_relation [instance, in Corelib.Classes.RelationClasses]
Involutions [section, in Corelib.ssr.ssrfun]
Involutions.A [variable, in Corelib.ssr.ssrfun]
Involutions.f [variable, in Corelib.ssr.ssrfun]
Involutions.Hf [variable, in Corelib.ssr.ssrfun]
involutive [definition, in Corelib.ssr.ssrfun]
inv_bij [lemma, in Corelib.ssr.ssrfun]
inv_inj [lemma, in Corelib.ssr.ssrfun]
inW_bij [lemma, in Corelib.ssr.ssrbool]
in_onS_can [lemma, in Corelib.ssr.ssrbool]
in_onW_can [lemma, in Corelib.ssr.ssrbool]
in_sig.P3 [variable, in Corelib.ssr.ssrbool]
in_sig.P2 [variable, in Corelib.ssr.ssrbool]
in_sig.P1 [variable, in Corelib.ssr.ssrbool]
in_sig.D3 [variable, in Corelib.ssr.ssrbool]
in_sig.D2 [variable, in Corelib.ssr.ssrbool]
in_sig.D1 [variable, in Corelib.ssr.ssrbool]
in_sig.T3 [variable, in Corelib.ssr.ssrbool]
in_sig.T2 [variable, in Corelib.ssr.ssrbool]
in_sig.T1 [variable, in Corelib.ssr.ssrbool]
in_sig [section, in Corelib.ssr.ssrbool]
in_inj_comp [lemma, in Corelib.ssr.ssrbool]
in_on2S [lemma, in Corelib.ssr.ssrbool]
in_on1lS [lemma, in Corelib.ssr.ssrbool]
in_on1S [lemma, in Corelib.ssr.ssrbool]
in_on2W [lemma, in Corelib.ssr.ssrbool]
in_on1lW [lemma, in Corelib.ssr.ssrbool]
in_on1W [lemma, in Corelib.ssr.ssrbool]
in_on2P [lemma, in Corelib.ssr.ssrbool]
in_on1lP [lemma, in Corelib.ssr.ssrbool]
in_on1P [lemma, in Corelib.ssr.ssrbool]
in_unkey [abbreviation, in Corelib.ssr.ssrbool]
in_simpl [lemma, in Corelib.ssr.ssrbool]
in_collective [lemma, in Corelib.ssr.ssrbool]
in_applicative [lemma, in Corelib.ssr.ssrbool]
in_mem [definition, in Corelib.ssr.ssrbool]
in_bounds [abbreviation, in Corelib.Array.ArrayAxioms]
in_right [abbreviation, in Corelib.Program.Utils]
in_left [abbreviation, in Corelib.Program.Utils]
in1T [lemma, in Corelib.ssr.ssrbool]
in1W [lemma, in Corelib.ssr.ssrbool]
in1_sig [lemma, in Corelib.ssr.ssrbool]
in2T [lemma, in Corelib.ssr.ssrbool]
in2W [lemma, in Corelib.ssr.ssrbool]
in2_sig [lemma, in Corelib.ssr.ssrbool]
in3T [lemma, in Corelib.ssr.ssrbool]
in3W [lemma, in Corelib.ssr.ssrbool]
in3_sig [lemma, in Corelib.ssr.ssrbool]
ipat [module, in Corelib.ssr.ssreflect]
[ ! _ ] (ssripat_scope) [notation, in Corelib.ssr.ssreflect]
[ 1 ! _ ] (ssripat_scope) [notation, in Corelib.ssr.ssreflect]
[ dup ] (ssripat_scope) [notation, in Corelib.ssr.ssreflect]
[ swap ] (ssripat_scope) [notation, in Corelib.ssr.ssreflect]
[ apply ] (ssripat_scope) [notation, in Corelib.ssr.ssreflect]
Irreflexive [record, in Corelib.Classes.RelationClasses]
Irreflexive [inductive, in Corelib.Classes.RelationClasses]
irreflexive [definition, in Corelib.ssr.ssrbool]
Irreflexive [record, in Corelib.Classes.CRelationClasses]
Irreflexive [inductive, in Corelib.Classes.CRelationClasses]
irreflexivity [projection, in Corelib.Classes.RelationClasses]
irreflexivity [constructor, in Corelib.Classes.RelationClasses]
irreflexivity [projection, in Corelib.Classes.CRelationClasses]
irreflexivity [constructor, in Corelib.Classes.CRelationClasses]
isSome [definition, in Corelib.ssr.ssrbool]
IsSucc [definition, in Corelib.Init.Peano]
isT [definition, in Corelib.ssr.ssrbool]
is_subrelation [projection, in Corelib.Classes.RelationClasses]
is_subrelation [constructor, in Corelib.Classes.RelationClasses]
is_true [definition, in Corelib.Init.Datatypes]
is_eq_true [constructor, in Corelib.Init.Datatypes]
is_inleft [definition, in Corelib.ssr.ssrbool]
is_left [definition, in Corelib.ssr.ssrbool]
is_inl [definition, in Corelib.ssr.ssrbool]
is_true_locked_true [lemma, in Corelib.ssr.ssrbool]
is_true_true [lemma, in Corelib.ssr.ssrbool]
is_even [definition, in Corelib.Numbers.Cyclic.Int63.Uint63Axioms]
is_zero [definition, in Corelib.Numbers.Cyclic.Int63.Uint63Axioms]
is_subrelation [projection, in Corelib.Classes.CRelationClasses]
is_subrelation [constructor, in Corelib.Classes.CRelationClasses]
is_finite [definition, in Corelib.Floats.PrimFloat]
is_infinity [definition, in Corelib.Floats.PrimFloat]
is_zero [definition, in Corelib.Floats.PrimFloat]
is_nan [definition, in Corelib.Floats.PrimFloat]
iter [definition, in Corelib.Init.Nat]
iter_pos [definition, in Corelib.Floats.SpecFloat]

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)