Standard Library | The Coq Proof Assistant

Global Index

(25958 entries)

Notation Index

F

J

K

T

X

Y

_

(999 entries)

Module Index

J

X

Y

_

other

(811 entries)

Variable Index

J

Q

V

X

Y

_

other

(1769 entries)

Library Index

K

X

Y

_

other

(587 entries)

Lemma Index

other

(11879 entries)

Constructor Index

K

Y

_

other

(960 entries)

Axiom Index

J

K

V

X

Y

_

other

(508 entries)

Inductive Index

X

Y

_

other

(307 entries)

Projection Index

G

K

X

Y

_

other

(479 entries)

Section Index

J

Q

X

Y

_

other

(495 entries)

Instance Index

J

V

X

Y

_

other

(905 entries)

Abbreviation Index

J

Y

_

other

(1199 entries)

Definition Index

_

other

(4894 entries)

Record Index

J

X

Y

_

other

(166 entries)

R (abbreviation)

R [in Coq.Reals.Rdefinitions]
Rabs_Rinv [in Coq.Reals.Rbasic_fun]
Raw.eqk [in Coq.FSets.FMapWeakList]
Raw.eqk [in Coq.FSets.FMapList]
Raw.eqke [in Coq.FSets.FMapWeakList]
Raw.eqke [in Coq.FSets.FMapList]
Raw.In [in Coq.FSets.FMapWeakList]
Raw.In [in Coq.FSets.FMapList]
Raw.Inf [in Coq.FSets.FMapList]
Raw.int [in Coq.FSets.FMapAVL]
Raw.ltk [in Coq.FSets.FMapList]
Raw.MapsTo [in Coq.FSets.FMapWeakList]
Raw.MapsTo [in Coq.FSets.FMapList]
Raw.NoDupA [in Coq.FSets.FMapWeakList]
Raw.oee' [in Coq.FSets.FMapWeakList]
Raw.oee' [in Coq.FSets.FMapList]
Raw.Proofs.eqk [in Coq.FSets.FMapAVL]
Raw.Proofs.eqke [in Coq.FSets.FMapAVL]
Raw.Proofs.ltk [in Coq.FSets.FMapAVL]
Raw.Proofs.map2_opt [in Coq.FSets.FMapAVL]
Raw.Sort [in Coq.FSets.FMapList]
Raw.t [in Coq.FSets.FMapAVL]
Raw.t [in Coq.FSets.FMapAVL]
reflect [in Coq.ssr.ssrbool]
ReflectF [in Coq.ssr.ssrbool]
ReflectT [in Coq.ssr.ssrbool]
refl_id [in Coq.Init.Datatypes]
refl_equal [in Coq.Init.Logic]
RefutablePropositionExtensionality [in Coq.Logic.PropExtensionalityFacts]
RelationalChoice [in Coq.Logic.ChoiceFacts]
rem [in Coq.Numbers.Cyclic.Int63.Sint63]
RepresentativeFunctionalChoice [in Coq.Logic.ChoiceFacts]
representative_boolean_partition [in Coq.Logic.ClassicalFacts]
Req_EM_T [in Coq.Reals.RIneq]
rev_length [in Coq.Lists.List]
rev_acc_rev [in Coq.Lists.List]
rev_acc [in Coq.Lists.List]
Rext [in Coq.setoid_ring.RealField]
right [in Coq.setoid_ring.Field_theory]
ring_correct [in Coq.setoid_ring.Field_theory]
ring_rw_pow_correct [in Coq.setoid_ring.Field_theory]
ring_rw_correct [in Coq.setoid_ring.Field_theory]
Rinv [in Coq.Reals.Rdefinitions]
Rinv_pow [in Coq.Reals.Rfunctions]
Rinv_Rdiv [in Coq.Reals.Rpower]
Rinv_mult_simpl [in Coq.Reals.RIneq]
Rinv_mult_distr [in Coq.Reals.RIneq]
Rinv_involutive [in Coq.Reals.RIneq]
Rinv_r_simpl_m [in Coq.Reals.RIneq]
Rinv_r_simpl_l [in Coq.Reals.RIneq]
Rinv_r_simpl_r [in Coq.Reals.RIneq]
Rle_Rinv [in Coq.Reals.RIneq]
Rlt [in Coq.Reals.Rdefinitions]
Rlt_Rminus [in Coq.Reals.RIneq]
RmaxLess1 [in Coq.Reals.Rbasic_fun]
RmaxLess2 [in Coq.Reals.Rbasic_fun]
RmaxSym [in Coq.Reals.Rbasic_fun]
Rminus_gt_0_lt [in Coq.Reals.RIneq]
Rminus_eq_0 [in Coq.Reals.RIneq]
Rmin_2 [in Coq.Reals.Ranalysis2]
Rmin_pos [in Coq.Reals.Ranalysis2]
Rmult [in Coq.Reals.Rdefinitions]
Ropp [in Coq.Reals.Rdefinitions]
Ropp_div [in Coq.Reals.RIneq]
Ropp_minus_distr' [in Coq.Reals.RIneq]
Ropp_div_den [in Coq.Reals.RIneq]
Ropp_inv_permute [in Coq.Reals.RIneq]
Rplus [in Coq.Reals.Rdefinitions]
Rplus_lt_pos [in Coq.Reals.DiscrR]
Rplus_sqr_eq_0_l [in Coq.Reals.RIneq]
Rplus_eq_R0 [in Coq.Reals.RIneq]
Rset [in Coq.setoid_ring.RealField]
Rsqr_inv [in Coq.Reals.R_sqr]
Rsqr_div [in Coq.Reals.R_sqr]
rtn1_trans_equiv [in Coq.Relations.Operators_Properties]
rtn1_trans [in Coq.Relations.Operators_Properties]
rtsn1_sym [in Coq.Relations.Operators_Properties]
rtsn1_trans [in Coq.Relations.Operators_Properties]
rtsn1_rts [in Coq.Relations.Operators_Properties]
rtsn1_trans [in Coq.Relations.Relation_Operators]
rtsn1_refl [in Coq.Relations.Relation_Operators]
rts_rtsn1_equiv [in Coq.Relations.Operators_Properties]
rts_rtsn1 [in Coq.Relations.Operators_Properties]
rts_rts1n_equiv [in Coq.Relations.Operators_Properties]
rts_rts1n [in Coq.Relations.Operators_Properties]
rts_1n_trans [in Coq.Relations.Operators_Properties]
rts1n_sym [in Coq.Relations.Operators_Properties]
rts1n_rts [in Coq.Relations.Operators_Properties]
rts1n_trans [in Coq.Relations.Relation_Operators]
rts1n_refl [in Coq.Relations.Relation_Operators]
rt1n_trans_equiv [in Coq.Relations.Operators_Properties]
rt1n_trans [in Coq.Relations.Operators_Properties]
R_rt1n [in Coq.Relations.Operators_Properties]
R_rtn1 [in Coq.Relations.Operators_Properties]
R_dist_mult_l [in Coq.Reals.Rfunctions]
R_dist_plus [in Coq.Reals.Rfunctions]
R_dist_tri [in Coq.Reals.Rfunctions]
R_dist_eq [in Coq.Reals.Rfunctions]
R_dist_refl [in Coq.Reals.Rfunctions]
R_dist_sym [in Coq.Reals.Rfunctions]
R_dist_pos [in Coq.Reals.Rfunctions]
R_dist [in Coq.Reals.Rfunctions]
R0 [in Coq.Reals.Rdefinitions]
R1 [in Coq.Reals.Rdefinitions]

Global Index

(25958 entries)

Notation Index

F

J

K

T

X

Y

_

(999 entries)

Module Index

J

X

Y

_

other

(811 entries)

Variable Index

J

Q

V

X

Y

_

other

(1769 entries)

Library Index

K

X

Y

_

other

(587 entries)

Lemma Index

other

(11879 entries)

Constructor Index

K

Y

_

other

(960 entries)

Axiom Index

J

K

V

X

Y

_

other

(508 entries)

Inductive Index

X

Y

_

other

(307 entries)

Projection Index

G

K

X

Y

_

other

(479 entries)

Section Index

J

Q

X

Y

_

other

(495 entries)

Instance Index

J

V

X

Y

_

other

(905 entries)

Abbreviation Index

J

Y

_

other

(1199 entries)

Definition Index

_

other

(4894 entries)

Record Index

J

X

Y

_

other

(166 entries)