Standard Library | The Coq Proof Assistant

Global Index

(68863 entries)

Notation Index

F

J

K

T

X

Y

_

(985 entries)

Binder Index

_

other

(44709 entries)

Module Index

J

X

Y

_

other

(761 entries)

Variable Index

H

J

Q

V

X

Y

_

other

(1497 entries)

Library Index

K

X

Y

_

other

(570 entries)

Lemma Index

other

(11380 entries)

Constructor Index

K

Y

_

other

(976 entries)

Axiom Index

K

V

X

Y

_

other

(603 entries)

Inductive Index

K

X

Y

_

other

(298 entries)

Projection Index

G

K

V

X

Y

_

other

(460 entries)

Section Index

H

J

Q

X

Y

_

other

(476 entries)

Instance Index

J

V

X

Y

_

other

(811 entries)

Abbreviation Index

J

Y

_

other

(1157 entries)

Definition Index

_

other

(4018 entries)

Record Index

J

V

X

Y

_

other

(162 entries)

R (definition)

R [in Coq.Vectors.Fin]
R [in Coq.Logic.Berardi]
Rabs [in Coq.Reals.Rbasic_fun]
Rabst_morphism [in Coq.Reals.ClassicalConstructiveReals]
Rabs_quot [in Coq.Reals.ClassicalConstructiveReals]
radd_term [in Coq.micromega.Tauto]
Ratan_seq [in Coq.Reals.Ratan]
ratom [in Coq.micromega.Tauto]
Raw.add [in Coq.FSets.FMapAVL]
Raw.assert_false [in Coq.FSets.FMapAVL]
Raw.at_least_one_then_f [in Coq.FSets.FMapWeakList]
Raw.at_least_one [in Coq.FSets.FMapWeakList]
Raw.at_least_right [in Coq.FSets.FMapWeakList]
Raw.at_least_left [in Coq.FSets.FMapWeakList]
Raw.at_least_one_then_f [in Coq.FSets.FMapList]
Raw.at_least_one [in Coq.FSets.FMapList]
Raw.bal [in Coq.FSets.FMapAVL]
Raw.cardinal [in Coq.FSets.FMapAVL]
Raw.check [in Coq.FSets.FMapWeakList]
Raw.combine [in Coq.FSets.FMapWeakList]
Raw.combine [in Coq.FSets.FMapList]
Raw.combine_r [in Coq.FSets.FMapWeakList]
Raw.combine_l [in Coq.FSets.FMapWeakList]
Raw.concat [in Coq.FSets.FMapAVL]
Raw.cons [in Coq.FSets.FMapAVL]
Raw.create [in Coq.FSets.FMapAVL]
Raw.elements [in Coq.FSets.FMapAVL]
Raw.elements [in Coq.FSets.FMapWeakList]
Raw.elements [in Coq.FSets.FMapList]
Raw.elements_aux [in Coq.FSets.FMapAVL]
Raw.empty [in Coq.FSets.FMapAVL]
Raw.Empty [in Coq.FSets.FMapWeakList]
Raw.empty [in Coq.FSets.FMapWeakList]
Raw.Empty [in Coq.FSets.FMapList]
Raw.empty [in Coq.FSets.FMapList]
Raw.equal [in Coq.FSets.FMapAVL]
Raw.equal [in Coq.FSets.FMapWeakList]
Raw.equal_end [in Coq.FSets.FMapAVL]
Raw.equal_cont [in Coq.FSets.FMapAVL]
Raw.equal_more [in Coq.FSets.FMapAVL]
Raw.Equivb [in Coq.FSets.FMapWeakList]
Raw.Equivb [in Coq.FSets.FMapList]
Raw.find [in Coq.FSets.FMapAVL]
Raw.fold [in Coq.FSets.FMapAVL]
Raw.fold_right_pair [in Coq.FSets.FMapWeakList]
Raw.fold_right_pair [in Coq.FSets.FMapList]
Raw.gt_tree [in Coq.FSets.FMapAVL]
Raw.height [in Coq.FSets.FMapAVL]
Raw.In0 [in Coq.FSets.FMapAVL]
Raw.is_empty [in Coq.FSets.FMapAVL]
Raw.is_empty [in Coq.FSets.FMapWeakList]
Raw.is_empty [in Coq.FSets.FMapList]
Raw.join [in Coq.FSets.FMapAVL]
Raw.key [in Coq.FSets.FMapAVL]
Raw.key [in Coq.FSets.FMapWeakList]
Raw.key [in Coq.FSets.FMapList]
Raw.lt_tree [in Coq.FSets.FMapAVL]
Raw.map [in Coq.FSets.FMapAVL]
Raw.map [in Coq.FSets.FMapWeakList]
Raw.map [in Coq.FSets.FMapList]
Raw.mapi [in Coq.FSets.FMapAVL]
Raw.mapi [in Coq.FSets.FMapWeakList]
Raw.mapi [in Coq.FSets.FMapList]
Raw.map_option [in Coq.FSets.FMapAVL]
Raw.map2 [in Coq.FSets.FMapAVL]
Raw.map2 [in Coq.FSets.FMapWeakList]
Raw.map2 [in Coq.FSets.FMapList]
Raw.map2_opt [in Coq.FSets.FMapAVL]
Raw.map2_alt [in Coq.FSets.FMapList]
Raw.map2_r [in Coq.FSets.FMapList]
Raw.map2_l [in Coq.FSets.FMapList]
Raw.mem [in Coq.FSets.FMapAVL]
Raw.merge [in Coq.FSets.FMapAVL]
Raw.of_pos [in Coq.Strings.OctalString]
Raw.of_pos [in Coq.Strings.HexString]
Raw.of_pos [in Coq.Strings.BinaryString]
Raw.option_cons [in Coq.FSets.FMapWeakList]
Raw.option_cons [in Coq.FSets.FMapList]
Raw.Proofs.Empty [in Coq.FSets.FMapAVL]
Raw.Proofs.Equivb [in Coq.FSets.FMapAVL]
Raw.Proofs.flatten_e [in Coq.FSets.FMapAVL]
Raw.Proofs.fold' [in Coq.FSets.FMapAVL]
Raw.Proofs.IfEq [in Coq.FSets.FMapAVL]
Raw.remove [in Coq.FSets.FMapAVL]
Raw.remove_min [in Coq.FSets.FMapAVL]
Raw.split [in Coq.FSets.FMapAVL]
Raw.Submap [in Coq.FSets.FMapWeakList]
Raw.submap [in Coq.FSets.FMapWeakList]
Raw.t [in Coq.FSets.FMapWeakList]
Raw.t [in Coq.FSets.FMapList]
Raw.to_N_of_pos [in Coq.Strings.OctalString]
Raw.to_N [in Coq.Strings.OctalString]
Raw.to_N_of_pos [in Coq.Strings.HexString]
Raw.to_N [in Coq.Strings.HexString]
Raw.to_N_of_pos [in Coq.Strings.BinaryString]
Raw.to_N [in Coq.Strings.BinaryString]
Raw2SetsOn.compare [in Coq.MSets.MSetInterface]
Raw2SetsOn.lt [in Coq.MSets.MSetInterface]
Raw2SetsOn.max_elt [in Coq.MSets.MSetInterface]
Raw2SetsOn.min_elt [in Coq.MSets.MSetInterface]
RbaseSymbolsImpl.R [in Coq.Reals.Rdefinitions]
RbaseSymbolsImpl.Rabst [in Coq.Reals.Rdefinitions]
RbaseSymbolsImpl.Rlt [in Coq.Reals.Rdefinitions]
RbaseSymbolsImpl.Rlt_def [in Coq.Reals.Rdefinitions]
RbaseSymbolsImpl.Rmult [in Coq.Reals.Rdefinitions]
RbaseSymbolsImpl.Rmult_def [in Coq.Reals.Rdefinitions]
RbaseSymbolsImpl.Ropp [in Coq.Reals.Rdefinitions]
RbaseSymbolsImpl.Ropp_def [in Coq.Reals.Rdefinitions]
RbaseSymbolsImpl.Rplus [in Coq.Reals.Rdefinitions]
RbaseSymbolsImpl.Rplus_def [in Coq.Reals.Rdefinitions]
RbaseSymbolsImpl.Rquot1 [in Coq.Reals.Rdefinitions]
RbaseSymbolsImpl.Rquot2 [in Coq.Reals.Rdefinitions]
RbaseSymbolsImpl.Rrepr [in Coq.Reals.Rdefinitions]
RbaseSymbolsImpl.R0 [in Coq.Reals.Rdefinitions]
RbaseSymbolsImpl.R0_def [in Coq.Reals.Rdefinitions]
RbaseSymbolsImpl.R1 [in Coq.Reals.Rdefinitions]
RbaseSymbolsImpl.R1_def [in Coq.Reals.Rdefinitions]
Rcompare [in Coq.Reals.ROrderedType]
rdeduce [in Coq.micromega.RMicromega]
Rdiv [in Coq.Reals.Rdefinitions]
recl [in Coq.Numbers.Cyclic.Int31.Int31]
recl_aux [in Coq.Numbers.Cyclic.Int31.Int31]
recr [in Coq.Numbers.Cyclic.Int31.Int31]
recrbis [in Coq.Numbers.Cyclic.Int31.Cyclic31]
recrbis_aux [in Coq.Numbers.Cyclic.Int31.Cyclic31]
recr_aux [in Coq.Numbers.Cyclic.Int31.Int31]
rectS [in Coq.Vectors.Fin]
rectS [in Coq.Vectors.VectorDef]
rect2 [in Coq.Vectors.Fin]
rect2 [in Coq.Vectors.VectorDef]
reduce [in Coq.btauto.Algebra]
reduce_aux [in Coq.btauto.Algebra]
reflexive [in Coq.ssr.ssrbool]
Reflexive [in Coq.Sets.Relations_1]
reflexive [in Coq.Relations.Relation_Definitions]
rel [in Coq.ssr.ssrbool]
Rel [in Coq.Sets.Partial_Order]
Relation [in Coq.Sets.Relations_1]
relation [in Coq.Relations.Relation_Definitions]
RelationalChoice_on [in Coq.Logic.ChoiceFacts]
relation_disjunction [in Coq.Classes.RelationClasses]
relation_conjunction [in Coq.Classes.RelationClasses]
relation_equivalence [in Coq.Classes.RelationClasses]
relation_disjunction [in Coq.Classes.CRelationClasses]
relation_conjunction [in Coq.Classes.CRelationClasses]
relation_equivalence [in Coq.Classes.CRelationClasses]
RelCompFun [in Coq.Classes.RelationPairs]
relpre [in Coq.ssr.ssrbool]
RelProd [in Coq.Classes.RelationPairs]
relU [in Coq.ssr.ssrbool]
rel_of_simpl [in Coq.ssr.ssrbool]
rel_prime_dec [in Coq.ZArith.Znumtheory]
rel_prime [in Coq.ZArith.Znumtheory]
Remainder [in Coq.ZArith.Zdiv]
Remainder [in Coq.ZArith.Zquot]
Remainder_alt [in Coq.ZArith.Zdiv]
Remainder_alt [in Coq.ZArith.Zquot]
remove [in Coq.Lists.List]
removeA [in Coq.Lists.SetoidList]
removelast [in Coq.Lists.List]
remove' [in Coq.Lists.List]
repeat [in Coq.Lists.List]
replace [in Coq.Vectors.VectorDef]
replace_order [in Coq.Vectors.VectorDef]
RepresentativeFunctionalChoice_on [in Coq.Logic.ChoiceFacts]
Reqb [in Coq.Reals.ROrderedType]
Req_constr [in Coq.Reals.ClassicalConstructiveReals]
respectful [in Coq.Classes.Morphisms]
respectful [in Coq.Classes.CMorphisms]
respectful_hetero [in Coq.Classes.Morphisms]
respectful_hetero [in Coq.Classes.CMorphisms]
respecting [in Coq.Classes.CEquivalence]
respecting [in Coq.Classes.Equivalence]
Reste [in Coq.Reals.Cos_rel]
Reste_E [in Coq.Reals.Exp_prop]
Reste1 [in Coq.Reals.Cos_rel]
Reste2 [in Coq.Reals.Cos_rel]
returnType [in Coq.ssr.ssreflect]
rev [in Coq.Init.Decimal]
rev [in Coq.Lists.List]
rev [in Coq.Init.Hexadecimal]
rev [in Coq.Vectors.VectorDef]
Reval_formula' [in Coq.micromega.RMicromega]
Reval_formula [in Coq.micromega.RMicromega]
Reval_op2 [in Coq.micromega.RMicromega]
Reval_expr [in Coq.micromega.RMicromega]
revapp [in Coq.Init.Decimal]
revapp [in Coq.Init.Hexadecimal]
rev_append [in Coq.Lists.List]
rev_left_loop [in Coq.ssr.ssrfun]
rev_right_loop [in Coq.ssr.ssrfun]
rev_append [in Coq.Vectors.VectorDef]
rev_append_tail [in Coq.Vectors.VectorDef]
rev' [in Coq.Lists.List]
Rfloor [in Coq.Reals.Cauchy.ConstructiveRcomplete]
Rge [in Coq.Reals.Rdefinitions]
Rgt [in Coq.Reals.Rdefinitions]
RHasMinMax.max [in Coq.Reals.Rminmax]
RHasMinMax.max_r [in Coq.Reals.Rminmax]
RHasMinMax.max_l [in Coq.Reals.Rminmax]
RHasMinMax.min [in Coq.Reals.Rminmax]
RHasMinMax.min_r [in Coq.Reals.Rminmax]
RHasMinMax.min_l [in Coq.Reals.Rminmax]
RiemannInt [in Coq.Reals.RiemannInt]
RiemannInt_SF [in Coq.Reals.RiemannInt_SF]
Riemann_integrable [in Coq.Reals.RiemannInt]
RightDistributivityImplicationOverDisjunction [in Coq.Logic.ClassicalFacts]
right_transitive [in Coq.ssr.ssrbool]
right_distributive [in Coq.ssr.ssrfun]
right_zero [in Coq.ssr.ssrfun]
right_loop [in Coq.ssr.ssrfun]
right_commutative [in Coq.ssr.ssrfun]
right_id [in Coq.ssr.ssrfun]
right_injective [in Coq.ssr.ssrfun]
right_inverse [in Coq.ssr.ssrfun]
ring_subst_niter [in Coq.setoid_ring.Ring_tac]
RinvImpl.Rinv [in Coq.Reals.Rdefinitions]
RinvImpl.Rinv_def [in Coq.Reals.Rdefinitions]
RinvN [in Coq.Reals.RiemannInt]
Rinv_quot [in Coq.Reals.ClassicalConstructiveReals]
Rle [in Coq.Reals.Rdefinitions]
Rle [in Coq.Reals.ClassicalDedekindReals]
Rln [in Coq.Reals.Rpower]
Rlt_epsilon [in Coq.Reals.ClassicalConstructiveReals]
Rmax [in Coq.Reals.Rbasic_fun]
Rmax_N [in Coq.Reals.Rseries]
Rmin [in Coq.Reals.Rbasic_fun]
Rminus [in Coq.Reals.Rdefinitions]
Rnegate [in Coq.micromega.RMicromega]
Rnormalise [in Coq.micromega.RMicromega]
Ropp_Ropp_IZR [in Coq.Reals.RIneq]
Rops_wd [in Coq.micromega.RingMicromega]
ror_cnf_opt [in Coq.micromega.Tauto]
ror_cnf [in Coq.micromega.Tauto]
ror_clause_cnf [in Coq.micromega.Tauto]
ror_clause [in Coq.micromega.Tauto]
round_nearest_even [in Coq.Floats.SpecFloat]
Rpower [in Coq.Reals.Rpower]
Rrepr_morphism [in Coq.Reals.ClassicalConstructiveReals]
RRle_abs [in Coq.Reals.Rbasic_fun]
Rsqr [in Coq.Reals.RIneq]
Rsqrt [in Coq.Reals.Rsqrt_def]
Rsrt [in Coq.micromega.RMicromega]
Rtail [in Coq.Reals.RList]
RTautoChecker [in Coq.micromega.RMicromega]
Rtheory [in Coq.nsatz.NsatzTactic]
runsat [in Coq.micromega.RMicromega]
Rup_nat [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
Rup_pos [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
RWeakChecker [in Coq.micromega.RMicromega]
RWitness [in Coq.micromega.RMicromega]
rxcnf [in Coq.micromega.Tauto]
R_dist [in Coq.Reals.Rfunctions]
r_list_pow [in Coq.setoid_ring.Ring_polynom]
R_met [in Coq.Reals.Rlimit]
R_of_Rcst [in Coq.micromega.RMicromega]
R_as_OT.compare_spec [in Coq.Reals.ROrderedType]
R_as_OT.compare [in Coq.Reals.ROrderedType]
R_as_OT.le [in Coq.Reals.ROrderedType]
R_as_OT.lt [in Coq.Reals.ROrderedType]
R_as_UBE.eqb_eq [in Coq.Reals.ROrderedType]
R_as_UBE.eqb [in Coq.Reals.ROrderedType]
R_as_UBE.eq [in Coq.Reals.ROrderedType]
R_as_UBE.t [in Coq.Reals.ROrderedType]
R2 [in Coq.nsatz.NsatzTactic]

Global Index

(68863 entries)

Notation Index

F

J

K

T

X

Y

_

(985 entries)

Binder Index

_

other

(44709 entries)

Module Index

J

X

Y

_

other

(761 entries)

Variable Index

H

J

Q

V

X

Y

_

other

(1497 entries)

Library Index

K

X

Y

_

other

(570 entries)

Lemma Index

other

(11380 entries)

Constructor Index

K

Y

_

other

(976 entries)

Axiom Index

K

V

X

Y

_

other

(603 entries)

Inductive Index

K

X

Y

_

other

(298 entries)

Projection Index

G

K

V

X

Y

_

other

(460 entries)

Section Index

H

J

Q

X

Y

_

other

(476 entries)

Instance Index

J

V

X

Y

_

other

(811 entries)

Abbreviation Index

J

Y

_

other

(1157 entries)

Definition Index

_

other

(4018 entries)

Record Index

J

V

X

Y

_

other

(162 entries)