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)

P

pair [constructor, in Corelib.Init.Datatypes]
pairT [abbreviation, in Corelib.Init.Datatypes]
pair_equal_spec [lemma, in Corelib.Init.Datatypes]
pair_andP [lemma, in Corelib.ssr.ssrbool]
pair_of_and [definition, in Corelib.ssr.ssrfun]
Params [record, in Corelib.Classes.CMorphisms]
Params [record, in Corelib.Classes.Morphisms]
PArrayNotations [module, in Corelib.Array.PrimArray]
_ .[ _ <- _ ] [notation, in Corelib.Array.PrimArray]
_ .[ _ ] [notation, in Corelib.Array.PrimArray]
parser [definition, in Corelib.Floats.PrimFloat]
parser [definition, in Corelib.Numbers.Cyclic.Int63.PrimInt63]
PartialApplication [record, in Corelib.Classes.CMorphisms]
PartialApplication [record, in Corelib.Classes.Morphisms]
PartialOrder [record, in Corelib.Classes.RelationClasses]
PartialOrder [inductive, in Corelib.Classes.RelationClasses]
PartialOrder [record, in Corelib.Classes.CRelationClasses]
PartialOrder [inductive, in Corelib.Classes.CRelationClasses]
PartialOrder_inverse [lemma, in Corelib.Classes.RelationClasses]
PartialOrder_StrictOrder [lemma, in Corelib.Classes.CMorphisms]
PartialOrder_proper_type [instance, in Corelib.Classes.CMorphisms]
PartialOrder_StrictOrder [lemma, in Corelib.Classes.Morphisms]
PartialOrder_proper [instance, in Corelib.Classes.Morphisms]
PartialOrder_inverse [lemma, in Corelib.Classes.CRelationClasses]
partial_order_antisym [instance, in Corelib.Classes.RelationClasses]
partial_order_equivalence [projection, in Corelib.Classes.RelationClasses]
partial_order_equivalence [constructor, in Corelib.Classes.RelationClasses]
partial_order_antisym [instance, in Corelib.Classes.CRelationClasses]
partial_order_equivalence [projection, in Corelib.Classes.CRelationClasses]
partial_order_equivalence [constructor, in Corelib.Classes.CRelationClasses]
Pattern [library]
pcancel [definition, in Corelib.ssr.ssrfun]
pcan_in_comp [lemma, in Corelib.ssr.ssrbool]
pcan_in_inj [lemma, in Corelib.ssr.ssrbool]
pcan_pcomp [lemma, in Corelib.ssr.ssrfun]
pcan_inj [lemma, in Corelib.ssr.ssrfun]
pcomp [definition, in Corelib.ssr.ssrfun]
Peano [library]
pequiv [definition, in Corelib.Classes.Equivalence]
PER [record, in Corelib.Classes.RelationClasses]
PER [record, in Corelib.Classes.CRelationClasses]
PER [record, in Corelib.Relations.Relation_Definitions]
PER_Transitive [projection, in Corelib.Classes.RelationClasses]
PER_Symmetric [projection, in Corelib.Classes.RelationClasses]
PER_type_morphism [instance, in Corelib.Classes.CMorphisms]
per_partial_app_type_morphism [instance, in Corelib.Classes.CMorphisms]
PER_morphism [instance, in Corelib.Classes.Morphisms]
per_partial_app_morphism [instance, in Corelib.Classes.Morphisms]
PER_Transitive [projection, in Corelib.Classes.CRelationClasses]
PER_Symmetric [projection, in Corelib.Classes.CRelationClasses]
per_trans [projection, in Corelib.Relations.Relation_Definitions]
per_sym [projection, in Corelib.Relations.Relation_Definitions]
ph [abbreviation, in Corelib.ssr.ssrbool]
ph [abbreviation, in Corelib.ssr.ssrbool]
Phant [constructor, in Corelib.ssr.ssreflect]
phant [inductive, in Corelib.ssr.ssreflect]
Phantom [constructor, in Corelib.ssr.ssreflect]
phantom [inductive, in Corelib.ssr.ssreflect]
phant_id [definition, in Corelib.ssr.ssrfun]
PInf [constructor, in Corelib.Floats.FloatClass]
plus [abbreviation, in Corelib.Init.Peano]
plus_succ_r_reverse [abbreviation, in Corelib.Init.Peano]
plus_0_r_reverse [abbreviation, in Corelib.Init.Peano]
plus_Sn_m [lemma, in Corelib.Init.Peano]
plus_n_Sm [lemma, in Corelib.Init.Peano]
plus_O_n [lemma, in Corelib.Init.Peano]
plus_n_O [lemma, in Corelib.Init.Peano]
PNormal [constructor, in Corelib.Floats.FloatClass]
pointwise_lifting [definition, in Corelib.Classes.RelationClasses]
pointwise_extension [definition, in Corelib.Classes.RelationClasses]
pointwise_subrelation [instance, in Corelib.Classes.CMorphisms]
pointwise_pointwise [lemma, in Corelib.Classes.CMorphisms]
pointwise_relation [definition, in Corelib.Classes.CMorphisms]
pointwise_subrelation [instance, in Corelib.Classes.Morphisms]
pointwise_pointwise [lemma, in Corelib.Classes.Morphisms]
pointwise_relation [definition, in Corelib.Classes.Morphisms]
pointwise_equivalence [instance, in Corelib.Classes.Equivalence]
pointwise_transitive [instance, in Corelib.Classes.Equivalence]
pointwise_symmetric [instance, in Corelib.Classes.Equivalence]
pointwise_reflexive [instance, in Corelib.Classes.Equivalence]
Pos [constructor, in Corelib.Init.Hexadecimal]
Pos [constructor, in Corelib.Init.Decimal]
Pos [module, in Corelib.BinNums.PosDef]
Pos [constructor, in Corelib.Numbers.Cyclic.Int63.PrimInt63]
PosDef [library]
positive [inductive, in Corelib.Numbers.BinNums]
positive_sind [definition, in Corelib.Numbers.BinNums]
positive_rec [definition, in Corelib.Numbers.BinNums]
positive_ind [definition, in Corelib.Numbers.BinNums]
positive_rect [definition, in Corelib.Numbers.BinNums]
pos_neg_int63 [inductive, in Corelib.Numbers.Cyclic.Int63.PrimInt63]
Pos.add [definition, in Corelib.BinNums.PosDef]
Pos.add_carry [definition, in Corelib.BinNums.PosDef]
Pos.compare [definition, in Corelib.BinNums.PosDef]
Pos.compare_cont [definition, in Corelib.BinNums.PosDef]
Pos.div2 [definition, in Corelib.BinNums.PosDef]
Pos.div2_up [definition, in Corelib.BinNums.PosDef]
Pos.double_pred_mask [definition, in Corelib.BinNums.PosDef]
Pos.double_mask [definition, in Corelib.BinNums.PosDef]
Pos.eqb [definition, in Corelib.BinNums.PosDef]
Pos.IsNeg [constructor, in Corelib.BinNums.PosDef]
Pos.IsNul [constructor, in Corelib.BinNums.PosDef]
Pos.IsPos [constructor, in Corelib.BinNums.PosDef]
Pos.iter [definition, in Corelib.BinNums.PosDef]
Pos.iter_op [definition, in Corelib.BinNums.PosDef]
Pos.land [definition, in Corelib.BinNums.PosDef]
Pos.ldiff [definition, in Corelib.BinNums.PosDef]
Pos.leb [definition, in Corelib.BinNums.PosDef]
Pos.lor [definition, in Corelib.BinNums.PosDef]
Pos.lxor [definition, in Corelib.BinNums.PosDef]
Pos.mask [inductive, in Corelib.BinNums.PosDef]
Pos.mask_sind [definition, in Corelib.BinNums.PosDef]
Pos.mask_rec [definition, in Corelib.BinNums.PosDef]
Pos.mask_ind [definition, in Corelib.BinNums.PosDef]
Pos.mask_rect [definition, in Corelib.BinNums.PosDef]
Pos.mul [definition, in Corelib.BinNums.PosDef]
Pos.Ndouble [definition, in Corelib.BinNums.PosDef]
Pos.Nsucc_double [definition, in Corelib.BinNums.PosDef]
Pos.of_succ_nat [definition, in Corelib.BinNums.PosDef]
Pos.pred_N [definition, in Corelib.BinNums.PosDef]
Pos.pred_double [definition, in Corelib.BinNums.PosDef]
Pos.sqrt [definition, in Corelib.BinNums.PosDef]
Pos.sqrtrem [definition, in Corelib.BinNums.PosDef]
Pos.sqrtrem_step [definition, in Corelib.BinNums.PosDef]
Pos.sub [definition, in Corelib.BinNums.PosDef]
Pos.sub_mask_carry [definition, in Corelib.BinNums.PosDef]
Pos.sub_mask [definition, in Corelib.BinNums.PosDef]
Pos.succ [definition, in Corelib.BinNums.PosDef]
Pos.succ_double_mask [definition, in Corelib.BinNums.PosDef]
Pos.to_nat [definition, in Corelib.BinNums.PosDef]
pow [definition, in Corelib.Init.Nat]
prec [definition, in Corelib.Floats.FloatOps]
pred [definition, in Corelib.Init.Nat]
pred [definition, in Corelib.ssr.ssrbool]
pred [abbreviation, in Corelib.Init.Peano]
predArgType [definition, in Corelib.ssr.ssrbool]
predC [definition, in Corelib.ssr.ssrbool]
predD [definition, in Corelib.ssr.ssrbool]
predI [definition, in Corelib.ssr.ssrbool]
predicate [abbreviation, in Corelib.Classes.RelationClasses]
PredicateSimplification [section, in Corelib.ssr.ssrbool]
PredicateSimplification.T [variable, in Corelib.ssr.ssrbool]
predicate_implication_preorder [instance, in Corelib.Classes.RelationClasses]
predicate_equivalence_equivalence [instance, in Corelib.Classes.RelationClasses]
predicate_union [definition, in Corelib.Classes.RelationClasses]
predicate_intersection [definition, in Corelib.Classes.RelationClasses]
predicate_implication [definition, in Corelib.Classes.RelationClasses]
predicate_equivalence [definition, in Corelib.Classes.RelationClasses]
predicate_exists [definition, in Corelib.Classes.RelationClasses]
predicate_all [definition, in Corelib.Classes.RelationClasses]
PredOfSimpl [module, in Corelib.ssr.ssrbool]
PredOfSimpl.coerce [definition, in Corelib.ssr.ssrbool]
predPredType [definition, in Corelib.ssr.ssrbool]
PredSortOfSimplCoercion [module, in Corelib.ssr.ssrbool]
PredSortOfSimplSignature [module, in Corelib.ssr.ssrbool]
PredSortOfSimplSignature.coerce [axiom, in Corelib.ssr.ssrbool]
predT [definition, in Corelib.ssr.ssrbool]
predType [record, in Corelib.ssr.ssrbool]
predU [definition, in Corelib.ssr.ssrbool]
pred_oapp [definition, in Corelib.ssr.ssrbool]
pred_key [inductive, in Corelib.ssr.ssrbool]
pred_of_mem [definition, in Corelib.ssr.ssrbool]
pred_of_argType [definition, in Corelib.ssr.ssrbool]
pred_of_simpl [abbreviation, in Corelib.ssr.ssrbool]
pred_sort [projection, in Corelib.ssr.ssrbool]
pred_Sn [lemma, in Corelib.Init.Peano]
pred0 [definition, in Corelib.ssr.ssrbool]
preim [definition, in Corelib.ssr.ssrbool]
Prelude [library]
PreOrder [record, in Corelib.Classes.RelationClasses]
PreOrder [record, in Corelib.Classes.CRelationClasses]
preorder [record, in Corelib.Relations.Relation_Definitions]
PreOrder_Transitive [projection, in Corelib.Classes.RelationClasses]
PreOrder_Reflexive [projection, in Corelib.Classes.RelationClasses]
PreOrder_Transitive [projection, in Corelib.Classes.CRelationClasses]
PreOrder_Reflexive [projection, in Corelib.Classes.CRelationClasses]
preord_trans [projection, in Corelib.Relations.Relation_Definitions]
preord_refl [projection, in Corelib.Relations.Relation_Definitions]
Pretype [module, in Ltac2.Constr]
Pretype.Flags [module, in Ltac2.Constr]
pre_symmetric [definition, in Corelib.ssr.ssrbool]
PrimArray [library]
PrimFloat [library]
PrimFloatNotations [module, in Corelib.Floats.PrimFloat]
PrimFloatNotationsInternalA [module, in Corelib.Floats.PrimFloat]
PrimFloatNotationsInternalB [module, in Corelib.Floats.PrimFloat]
_ / _ (float_scope) [notation, in Corelib.Floats.PrimFloat]
_ - _ (float_scope) [notation, in Corelib.Floats.PrimFloat]
_ + _ (float_scope) [notation, in Corelib.Floats.PrimFloat]
_ * _ (float_scope) [notation, in Corelib.Floats.PrimFloat]
_ ?= _ (float_scope) [notation, in Corelib.Floats.PrimFloat]
_ <=? _ (float_scope) [notation, in Corelib.Floats.PrimFloat]
_ <? _ (float_scope) [notation, in Corelib.Floats.PrimFloat]
_ =? _ (float_scope) [notation, in Corelib.Floats.PrimFloat]
- _ (float_scope) [notation, in Corelib.Floats.PrimFloat]
PrimInt63 [library]
PrimInt63Notations [module, in Corelib.Numbers.Cyclic.Int63.PrimInt63]
PrimString [library]
PrimStringAxioms [library]
Prim2SF [definition, in Corelib.Floats.FloatOps]
Prim2SF_inj [lemma, in Corelib.Floats.FloatAxioms]
Prim2SF_SF2Prim [axiom, in Corelib.Floats.FloatAxioms]
Prim2SF_valid [axiom, in Corelib.Floats.FloatAxioms]
printer [definition, in Corelib.Floats.PrimFloat]
printer [definition, in Corelib.Numbers.Cyclic.Int63.PrimInt63]
Printf [library]
prod [inductive, in Corelib.Init.Datatypes]
ProdSigT [section, in Corelib.Init.Specif]
ProdSigT.A [variable, in Corelib.Init.Specif]
ProdSigT.B [variable, in Corelib.Init.Specif]
prodT [abbreviation, in Corelib.Init.Datatypes]
prodT_ind [abbreviation, in Corelib.Init.Datatypes]
prodT_rec [abbreviation, in Corelib.Init.Datatypes]
prodT_rect [abbreviation, in Corelib.Init.Datatypes]
prod_sind [definition, in Corelib.Init.Datatypes]
prod_rec [definition, in Corelib.Init.Datatypes]
prod_ind [definition, in Corelib.Init.Datatypes]
prod_rect [definition, in Corelib.Init.Datatypes]
prod_sigT_prod [lemma, in Corelib.Init.Specif]
prod_of_sigT [definition, in Corelib.Init.Specif]
Proj [library]
projections [section, in Corelib.Init.Datatypes]
Projections [section, in Corelib.Init.Specif]
Projections [section, in Corelib.Init.Logic]
projections.A [variable, in Corelib.Init.Datatypes]
Projections.A [variable, in Corelib.Init.Specif]
Projections.A [variable, in Corelib.Init.Logic]
projections.B [variable, in Corelib.Init.Datatypes]
Projections.P [variable, in Corelib.Init.Specif]
Projections.P [variable, in Corelib.Init.Logic]
Projections2 [section, in Corelib.Init.Specif]
Projections2.A [variable, in Corelib.Init.Specif]
Projections2.P [variable, in Corelib.Init.Specif]
Projections2.Q [variable, in Corelib.Init.Specif]
projT1 [definition, in Corelib.Init.Specif]
projT1_of_sigT2_eq [definition, in Corelib.Init.Specif]
projT1_eq [definition, in Corelib.Init.Specif]
projT2 [definition, in Corelib.Init.Specif]
projT2_of_sigT2_eq [definition, in Corelib.Init.Specif]
projT2_eq [definition, in Corelib.Init.Specif]
projT3 [definition, in Corelib.Init.Specif]
projT3_eq [definition, in Corelib.Init.Specif]
proj1 [lemma, in Corelib.Init.Logic]
proj1_sig_of_sig2_eq [definition, in Corelib.Init.Specif]
proj1_sig_eq [definition, in Corelib.Init.Specif]
proj1_sig [definition, in Corelib.Init.Specif]
proj2 [lemma, in Corelib.Init.Logic]
proj2_sig_of_sig2_eq [definition, in Corelib.Init.Specif]
proj2_sig_eq [definition, in Corelib.Init.Specif]
proj2_sig [definition, in Corelib.Init.Specif]
proj3_sig_eq [definition, in Corelib.Init.Specif]
proj3_sig [definition, in Corelib.Init.Specif]
Proper [record, in Corelib.Classes.CMorphisms]
Proper [inductive, in Corelib.Classes.CMorphisms]
Proper [section, in Corelib.Classes.CMorphisms]
Proper [record, in Corelib.Classes.Morphisms]
Proper [inductive, in Corelib.Classes.Morphisms]
Proper [section, in Corelib.Classes.Morphisms]
ProperNotations [module, in Corelib.Classes.CMorphisms]
ProperNotations [module, in Corelib.Classes.Morphisms]
_ --> _ (signatureT_scope) [notation, in Corelib.Classes.CMorphisms]
_ ==> _ (signatureT_scope) [notation, in Corelib.Classes.CMorphisms]
_ ++> _ (signatureT_scope) [notation, in Corelib.Classes.CMorphisms]
_ --> _ (signature_scope) [notation, in Corelib.Classes.Morphisms]
_ ==> _ (signature_scope) [notation, in Corelib.Classes.Morphisms]
_ ++> _ (signature_scope) [notation, in Corelib.Classes.Morphisms]
ProperProxy [record, in Corelib.Classes.CMorphisms]
ProperProxy [inductive, in Corelib.Classes.CMorphisms]
ProperProxy [record, in Corelib.Classes.Morphisms]
ProperProxy [inductive, in Corelib.Classes.Morphisms]
proper_sym_arrow_iffT_2 [lemma, in Corelib.Classes.CMorphisms]
proper_sym_impl_iff_2 [lemma, in Corelib.Classes.CMorphisms]
proper_sym_arrow_iffT [lemma, in Corelib.Classes.CMorphisms]
proper_sym_impl_iff [lemma, in Corelib.Classes.CMorphisms]
proper_sym_flip_2 [lemma, in Corelib.Classes.CMorphisms]
proper_sym_flip [lemma, in Corelib.Classes.CMorphisms]
proper_normalizes_proper [lemma, in Corelib.Classes.CMorphisms]
proper_proper [instance, in Corelib.Classes.CMorphisms]
proper_eq [lemma, in Corelib.Classes.CMorphisms]
proper_flip_proper [definition, in Corelib.Classes.CMorphisms]
proper_subrelation_proper_arrow [instance, in Corelib.Classes.CMorphisms]
proper_proper_proxy [lemma, in Corelib.Classes.CMorphisms]
proper_proxy [projection, in Corelib.Classes.CMorphisms]
proper_proxy [constructor, in Corelib.Classes.CMorphisms]
proper_prf [projection, in Corelib.Classes.CMorphisms]
proper_prf [constructor, in Corelib.Classes.CMorphisms]
proper_sym_impl_iff_2 [lemma, in Corelib.Classes.Morphisms]
proper_sym_impl_iff [lemma, in Corelib.Classes.Morphisms]
proper_sym_flip_2 [lemma, in Corelib.Classes.Morphisms]
proper_sym_flip [lemma, in Corelib.Classes.Morphisms]
proper_normalizes_proper [lemma, in Corelib.Classes.Morphisms]
proper_proper [instance, in Corelib.Classes.Morphisms]
proper_eq [lemma, in Corelib.Classes.Morphisms]
proper_flip_proper [definition, in Corelib.Classes.Morphisms]
proper_subrelation_proper [instance, in Corelib.Classes.Morphisms]
proper_proper_proxy [lemma, in Corelib.Classes.Morphisms]
proper_proxy [projection, in Corelib.Classes.Morphisms]
proper_proxy [constructor, in Corelib.Classes.Morphisms]
proper_prf [projection, in Corelib.Classes.Morphisms]
proper_prf [constructor, in Corelib.Classes.Morphisms]
Proper.A [variable, in Corelib.Classes.CMorphisms]
Proper.A [variable, in Corelib.Classes.Morphisms]
Proper.B [variable, in Corelib.Classes.Morphisms]
Proper.U [variable, in Corelib.Classes.Morphisms]
prop_on2 [definition, in Corelib.ssr.ssrbool]
prop_on1 [definition, in Corelib.ssr.ssrbool]
prop_in3 [definition, in Corelib.ssr.ssrbool]
prop_in21 [definition, in Corelib.ssr.ssrbool]
prop_in12 [definition, in Corelib.ssr.ssrbool]
prop_in111 [definition, in Corelib.ssr.ssrbool]
prop_in2 [definition, in Corelib.ssr.ssrbool]
prop_in11 [definition, in Corelib.ssr.ssrbool]
prop_in1 [definition, in Corelib.ssr.ssrbool]
prop_for [definition, in Corelib.ssr.ssrbool]
prop_congr [lemma, in Corelib.ssr.ssrbool]
protect_term [definition, in Corelib.ssr.ssreflect]
Pstring [library]
PStringNotations [module, in Corelib.Strings.PrimString]
PStringNotations.id_string [definition, in Corelib.Strings.PrimString]
PStringNotations.string_wrap [projection, in Corelib.Strings.PrimString]
PStringNotations.string_wrapper [record, in Corelib.Strings.PrimString]
PSubn [constructor, in Corelib.Floats.FloatClass]
PZero [constructor, in Corelib.Floats.FloatClass]

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)