Standard Library | The Coq Proof Assistant

Global Index

(22787 entries)

Notation Index

F

J

K

T

X

Y

_

(729 entries)

Module Index

J

X

Y

_

other

(767 entries)

Variable Index

H

J

Q

V

X

Y

_

other

(1469 entries)

Library Index

K

X

Y

_

other

(561 entries)

Lemma Index

other

(11410 entries)

Constructor Index

K

Q

Y

_

other

(526 entries)

Axiom Index

J

K

V

X

Y

_

other

(359 entries)

Inductive Index

Q

X

Y

_

other

(209 entries)

Projection Index

G

K

V

X

Y

_

other

(403 entries)

Section Index

H

J

Q

X

Y

_

other

(393 entries)

Instance Index

J

V

X

Y

_

other

(789 entries)

Abbreviation Index

J

V

Y

_

other

(1186 entries)

Definition Index

_

other

(3882 entries)

Record Index

J

K

V

X

Y

_

other

(104 entries)

other (notation)

_ <=? _ (char_scope) [in Stdlib.Strings.Ascii]
_ <? _ (char_scope) [in Stdlib.Strings.Ascii]
_ ?= _ (char_scope) [in Stdlib.Strings.Ascii]
_ =? _ (char_scope) [in Stdlib.Strings.Ascii]
_ * _ (ConstructiveReals) [in Stdlib.Reals.Abstract.ConstructiveReals]
_ - _ (ConstructiveReals) [in Stdlib.Reals.Abstract.ConstructiveReals]
_ + _ (ConstructiveReals) [in Stdlib.Reals.Abstract.ConstructiveReals]
_ ≶ _ (ConstructiveReals) [in Stdlib.Reals.Abstract.ConstructiveReals]
_ == _ (ConstructiveReals) [in Stdlib.Reals.Abstract.ConstructiveReals]
_ < _ < _ (ConstructiveReals) [in Stdlib.Reals.Abstract.ConstructiveReals]
_ <= _ <= _ (ConstructiveReals) [in Stdlib.Reals.Abstract.ConstructiveReals]
_ <= _ (ConstructiveReals) [in Stdlib.Reals.Abstract.ConstructiveReals]
_ < _ (ConstructiveReals) [in Stdlib.Reals.Abstract.ConstructiveReals]
- _ (ConstructiveReals) [in Stdlib.Reals.Abstract.ConstructiveReals]
/ _ (ConstructiveReals) [in Stdlib.Reals.Abstract.ConstructiveReals]
0 (ConstructiveReals) [in Stdlib.Reals.Abstract.ConstructiveReals]
1 (ConstructiveReals) [in Stdlib.Reals.Abstract.ConstructiveReals]
10 (ConstructiveReals) [in Stdlib.Reals.Abstract.ConstructiveReals]
2 (ConstructiveReals) [in Stdlib.Reals.Abstract.ConstructiveReals]
3 (ConstructiveReals) [in Stdlib.Reals.Abstract.ConstructiveReals]
4 (ConstructiveReals) [in Stdlib.Reals.Abstract.ConstructiveReals]
5 (ConstructiveReals) [in Stdlib.Reals.Abstract.ConstructiveReals]
6 (ConstructiveReals) [in Stdlib.Reals.Abstract.ConstructiveReals]
7 (ConstructiveReals) [in Stdlib.Reals.Abstract.ConstructiveReals]
8 (ConstructiveReals) [in Stdlib.Reals.Abstract.ConstructiveReals]
9 (ConstructiveReals) [in Stdlib.Reals.Abstract.ConstructiveReals]
_ - _ (CReal_scope) [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
- _ (CReal_scope) [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
_ + _ (CReal_scope) [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
2 (CReal_scope) [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
1 (CReal_scope) [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
0 (CReal_scope) [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
_ == _ (CReal_scope) [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
_ < _ <= _ (CReal_scope) [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
_ < _ < _ (CReal_scope) [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
_ <= _ < _ (CReal_scope) [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
_ <= _ <= _ (CReal_scope) [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
_ >= _ (CReal_scope) [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
_ <= _ (CReal_scope) [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
_ # _ (CReal_scope) [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
_ > _ (CReal_scope) [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
_ < _ (CReal_scope) [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
/ _ (CReal_scope) [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
_ * _ (CReal_scope) [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
_ =~= _ (equiv_scope) [in Stdlib.Classes.CEquivalence]
_ =/= _ (equiv_scope) [in Stdlib.Classes.CEquivalence]
_ === _ (equiv_scope) [in Stdlib.Classes.CEquivalence]
_ <> _ (equiv_scope) [in Stdlib.Classes.EquivDec]
_ == _ (equiv_scope) [in Stdlib.Classes.EquivDec]
_ ||| _ (lazy_bool_scope) [in Stdlib.Bool.Bool]
_ &&& _ (lazy_bool_scope) [in Stdlib.Bool.Bool]
_ +++ _ (list_scope) [in Stdlib.micromega.Refl]
_ mod _ (nat_scope) [in Stdlib.Arith.PeanoNat]
_ / _ (nat_scope) [in Stdlib.Arith.PeanoNat]
_ ?= _ (nat_scope) [in Stdlib.Arith.PeanoNat]
_ <? _ (nat_scope) [in Stdlib.Arith.PeanoNat]
_ <=? _ (nat_scope) [in Stdlib.Arith.PeanoNat]
_ =? _ (nat_scope) [in Stdlib.Arith.PeanoNat]
_ ^ _ (nat_scope) [in Stdlib.Arith.PeanoNat]
( _ | _ ) (N_scope) [in Stdlib.NArith.BinNat]
_ mod _ (N_scope) [in Stdlib.NArith.BinNat]
_ / _ (N_scope) [in Stdlib.NArith.BinNat]
_ <? _ (N_scope) [in Stdlib.NArith.BinNat]
_ <=? _ (N_scope) [in Stdlib.NArith.BinNat]
_ =? _ (N_scope) [in Stdlib.NArith.BinNat]
_ < _ <= _ (N_scope) [in Stdlib.NArith.BinNat]
_ < _ < _ (N_scope) [in Stdlib.NArith.BinNat]
_ <= _ < _ (N_scope) [in Stdlib.NArith.BinNat]
_ <= _ <= _ (N_scope) [in Stdlib.NArith.BinNat]
_ > _ (N_scope) [in Stdlib.NArith.BinNat]
_ >= _ (N_scope) [in Stdlib.NArith.BinNat]
_ < _ (N_scope) [in Stdlib.NArith.BinNat]
_ <= _ (N_scope) [in Stdlib.NArith.BinNat]
_ ?= _ (N_scope) [in Stdlib.NArith.BinNat]
_ ^ _ (N_scope) [in Stdlib.NArith.BinNat]
_ * _ (N_scope) [in Stdlib.NArith.BinNat]
_ - _ (N_scope) [in Stdlib.NArith.BinNat]
_ + _ (N_scope) [in Stdlib.NArith.BinNat]
_ #2 (pair_scope) [in Stdlib.FSets.FMapAVL]
_ #1 (pair_scope) [in Stdlib.FSets.FMapAVL]
_ #2 (pair_scope) [in Stdlib.Numbers.Integer.NatPairs.ZNatPairs]
_ #1 (pair_scope) [in Stdlib.Numbers.Integer.NatPairs.ZNatPairs]
( _ | _ ) (positive_scope) [in Stdlib.PArith.BinPos]
_ < _ <= _ (positive_scope) [in Stdlib.PArith.BinPos]
_ < _ < _ (positive_scope) [in Stdlib.PArith.BinPos]
_ <= _ < _ (positive_scope) [in Stdlib.PArith.BinPos]
_ <= _ <= _ (positive_scope) [in Stdlib.PArith.BinPos]
_ > _ (positive_scope) [in Stdlib.PArith.BinPos]
_ >= _ (positive_scope) [in Stdlib.PArith.BinPos]
_ < _ (positive_scope) [in Stdlib.PArith.BinPos]
_ <= _ (positive_scope) [in Stdlib.PArith.BinPos]
_ <? _ (positive_scope) [in Stdlib.PArith.BinPos]
_ <=? _ (positive_scope) [in Stdlib.PArith.BinPos]
_ =? _ (positive_scope) [in Stdlib.PArith.BinPos]
_ ?= _ (positive_scope) [in Stdlib.PArith.BinPos]
_ ^ _ (positive_scope) [in Stdlib.PArith.BinPos]
_ * _ (positive_scope) [in Stdlib.PArith.BinPos]
_ - _ (positive_scope) [in Stdlib.PArith.BinPos]
_ + _ (positive_scope) [in Stdlib.PArith.BinPos]
[ _ ] (Qc_scope) [in Stdlib.QArith.Qcabs]
_ ^ _ (Qc_scope) [in Stdlib.QArith.Qcanon]
_ / _ (Qc_scope) [in Stdlib.QArith.Qcanon]
/ _ (Qc_scope) [in Stdlib.QArith.Qcanon]
_ - _ (Qc_scope) [in Stdlib.QArith.Qcanon]
- _ (Qc_scope) [in Stdlib.QArith.Qcanon]
_ * _ (Qc_scope) [in Stdlib.QArith.Qcanon]
_ + _ (Qc_scope) [in Stdlib.QArith.Qcanon]
_ ?= _ (Qc_scope) [in Stdlib.QArith.Qcanon]
_ < _ < _ (Qc_scope) [in Stdlib.QArith.Qcanon]
_ <= _ <= _ (Qc_scope) [in Stdlib.QArith.Qcanon]
_ >= _ (Qc_scope) [in Stdlib.QArith.Qcanon]
_ > _ (Qc_scope) [in Stdlib.QArith.Qcanon]
_ <= _ (Qc_scope) [in Stdlib.QArith.Qcanon]
_ < _ (Qc_scope) [in Stdlib.QArith.Qcanon]
1 (Qc_scope) [in Stdlib.QArith.Qcanon]
0 (Qc_scope) [in Stdlib.QArith.Qcanon]
_ ^ _ (Q_scope) [in Stdlib.QArith.QArith_base]
_ / _ (Q_scope) [in Stdlib.QArith.QArith_base]
/ _ (Q_scope) [in Stdlib.QArith.QArith_base]
_ * _ (Q_scope) [in Stdlib.QArith.QArith_base]
_ - _ (Q_scope) [in Stdlib.QArith.QArith_base]
- _ (Q_scope) [in Stdlib.QArith.QArith_base]
_ + _ (Q_scope) [in Stdlib.QArith.QArith_base]
_ ?= _ (Q_scope) [in Stdlib.QArith.QArith_base]
_ < _ < _ (Q_scope) [in Stdlib.QArith.QArith_base]
_ < _ <= _ (Q_scope) [in Stdlib.QArith.QArith_base]
_ <= _ < _ (Q_scope) [in Stdlib.QArith.QArith_base]
_ <= _ <= _ (Q_scope) [in Stdlib.QArith.QArith_base]
_ >= _ (Q_scope) [in Stdlib.QArith.QArith_base]
_ > _ (Q_scope) [in Stdlib.QArith.QArith_base]
_ <= _ (Q_scope) [in Stdlib.QArith.QArith_base]
_ < _ (Q_scope) [in Stdlib.QArith.QArith_base]
_ == _ (Q_scope) [in Stdlib.QArith.QArith_base]
_ # _ (Q_scope) [in Stdlib.QArith.QArith_base]
/ _ (Rfun_scope) [in Stdlib.Reals.Ranalysis1]
_ o _ (Rfun_scope) [in Stdlib.Reals.Ranalysis1]
_ / _ (Rfun_scope) [in Stdlib.Reals.Ranalysis1]
_ - _ (Rfun_scope) [in Stdlib.Reals.Ranalysis1]
_ * _ (Rfun_scope) [in Stdlib.Reals.Ranalysis1]
- _ (Rfun_scope) [in Stdlib.Reals.Ranalysis1]
_ + _ (Rfun_scope) [in Stdlib.Reals.Ranalysis1]
_ ^Z _ (R_scope) [in Stdlib.Reals.Rfunctions]
_ ^ _ (R_scope) [in Stdlib.Reals.Rfunctions]
_ / _ (R_scope) [in Stdlib.Reals.Rdefinitions]
/ _ (R_scope) [in Stdlib.Reals.Rdefinitions]
_ < _ <= _ (R_scope) [in Stdlib.Reals.Rdefinitions]
_ < _ < _ (R_scope) [in Stdlib.Reals.Rdefinitions]
_ <= _ < _ (R_scope) [in Stdlib.Reals.Rdefinitions]
_ <= _ <= _ (R_scope) [in Stdlib.Reals.Rdefinitions]
_ > _ (R_scope) [in Stdlib.Reals.Rdefinitions]
_ >= _ (R_scope) [in Stdlib.Reals.Rdefinitions]
_ <= _ (R_scope) [in Stdlib.Reals.Rdefinitions]
_ - _ (R_scope) [in Stdlib.Reals.Rdefinitions]
_ < _ (R_scope) [in Stdlib.Reals.Rdefinitions]
- _ (R_scope) [in Stdlib.Reals.Rdefinitions]
_ * _ (R_scope) [in Stdlib.Reals.Rdefinitions]
_ + _ (R_scope) [in Stdlib.Reals.Rdefinitions]
_ ² (R_scope) [in Stdlib.Reals.RIneq]
_ * _ (signature_scope) [in Stdlib.Classes.RelationPairs]
_ @@2 (signature_scope) [in Stdlib.Classes.RelationPairs]
_ @@1 (signature_scope) [in Stdlib.Classes.RelationPairs]
_ @@ _ (signature_scope) [in Stdlib.Classes.RelationPairs]
_ ++ _ (string_scope) [in Stdlib.Strings.String]
_ <=? _ (string_scope) [in Stdlib.Strings.String]
_ <? _ (string_scope) [in Stdlib.Strings.String]
_ ?= _ (string_scope) [in Stdlib.Strings.String]
_ =? _ (string_scope) [in Stdlib.Strings.String]
_ =~= _ (type_scope) [in Stdlib.Classes.SetoidClass]
_ =/= _ (type_scope) [in Stdlib.Classes.SetoidClass]
_ == _ (type_scope) [in Stdlib.Classes.SetoidClass]
() (type_scope) [in Stdlib.Program.Syntax]
_ ^ _ (type_scope) [in Stdlib.Numbers.NaryFunctions]
_ ^^ _ --> _ (type_scope) [in Stdlib.Numbers.NaryFunctions]
_ ≠ _ (type_scope) [in Stdlib.Unicode.Utf8_core]
¬ _ (type_scope) [in Stdlib.Unicode.Utf8_core]
_ ↔ _ (type_scope) [in Stdlib.Unicode.Utf8_core]
_ → _ (type_scope) [in Stdlib.Unicode.Utf8_core]
_ ∧ _ (type_scope) [in Stdlib.Unicode.Utf8_core]
_ ∨ _ (type_scope) [in Stdlib.Unicode.Utf8_core]
∃ _ .. _ , _ (type_scope) [in Stdlib.Unicode.Utf8_core]
∀ _ .. _ , _ (type_scope) [in Stdlib.Unicode.Utf8_core]
_ *c _ (uint63_scope) [in Stdlib.Numbers.Cyclic.Int63.Cyclic63]
_ ≡ _ (uint63_scope) [in Stdlib.Numbers.Cyclic.Int63.Uint63]
[-| _ |] (uint63_scope) [in Stdlib.Numbers.Cyclic.Int63.Uint63]
[+| _ |] (uint63_scope) [in Stdlib.Numbers.Cyclic.Int63.Uint63]
_ < _ <= _ (Z_scope) [in Stdlib.ZArith.BinInt]
_ < _ < _ (Z_scope) [in Stdlib.ZArith.BinInt]
_ <= _ < _ (Z_scope) [in Stdlib.ZArith.BinInt]
_ <= _ <= _ (Z_scope) [in Stdlib.ZArith.BinInt]
_ > _ (Z_scope) [in Stdlib.ZArith.BinInt]
_ >= _ (Z_scope) [in Stdlib.ZArith.BinInt]
_ < _ (Z_scope) [in Stdlib.ZArith.BinInt]
_ <= _ (Z_scope) [in Stdlib.ZArith.BinInt]
( _ | _ ) (Z_scope) [in Stdlib.ZArith.BinInt]
_ >? _ (Z_scope) [in Stdlib.ZArith.BinInt]
_ >=? _ (Z_scope) [in Stdlib.ZArith.BinInt]
_ <? _ (Z_scope) [in Stdlib.ZArith.BinInt]
_ <=? _ (Z_scope) [in Stdlib.ZArith.BinInt]
_ =? _ (Z_scope) [in Stdlib.ZArith.BinInt]
_ ?= _ (Z_scope) [in Stdlib.ZArith.BinInt]
_ ÷ _ (Z_scope) [in Stdlib.ZArith.BinInt]
_ mod _ (Z_scope) [in Stdlib.ZArith.BinInt]
_ / _ (Z_scope) [in Stdlib.ZArith.BinInt]
_ ^ _ (Z_scope) [in Stdlib.ZArith.BinInt]
_ * _ (Z_scope) [in Stdlib.ZArith.BinInt]
_ - _ (Z_scope) [in Stdlib.ZArith.BinInt]
- _ (Z_scope) [in Stdlib.ZArith.BinInt]
_ + _ (Z_scope) [in Stdlib.ZArith.BinInt]
_ ^^ _ (Z_scope) [in Stdlib.ZArith.Zpow_alt]
_ [@ _ ] [in Stdlib.Vectors.VectorDef]
_ :: _ [in Stdlib.Vectors.VectorDef]
_ <>b _ [in Stdlib.Classes.SetoidDec]
_ ==b _ [in Stdlib.Classes.SetoidDec]
_ =/= _ [in Stdlib.Classes.SetoidDec]
_ == _ [in Stdlib.Classes.SetoidDec]
_ \ _ [in Stdlib.rtauto.Bintree]
_ =_D _ [in Stdlib.Reals.Rtopology]
_ + _ [in Stdlib.Structures.OrdersTac]
_ ^ _ [in Stdlib.Numbers.NatInt.NZDomain]
_ ~= _ [in Stdlib.Program.Equality]
_ ^ _ [in Stdlib.setoid_ring.Algebra_syntax]
_ == _ [in Stdlib.setoid_ring.Algebra_syntax]
_ - _ [in Stdlib.setoid_ring.Algebra_syntax]
_ * _ [in Stdlib.setoid_ring.Algebra_syntax]
_ + _ [in Stdlib.setoid_ring.Algebra_syntax]
_ <>b _ [in Stdlib.Classes.EquivDec]
_ ==b _ [in Stdlib.Classes.EquivDec]
_ \\// _ [in Stdlib.rtauto.Rtauto]
_ //\\ _ [in Stdlib.rtauto.Rtauto]
_ =>> _ [in Stdlib.rtauto.Rtauto]
_ .1 [in Stdlib.Logic.ClassicalFacts]
_ ≥ _ [in Stdlib.Unicode.Utf8]
_ ≤ _ [in Stdlib.Unicode.Utf8]
_ || _ [in Stdlib.Strings.HexString]
Set [in Stdlib.Logic.SetIsType]
_==_ [in Stdlib.setoid_ring.Algebra_syntax]
_-_ [in Stdlib.setoid_ring.Algebra_syntax]
_*_ [in Stdlib.setoid_ring.Algebra_syntax]
_+_ [in Stdlib.setoid_ring.Algebra_syntax]
# [in Stdlib.rtauto.Rtauto]
( _ ; _ ) [in Stdlib.Logic.ClassicalFacts]
() [in Stdlib.Program.Syntax]
-_ [in Stdlib.setoid_ring.Algebra_syntax]
- _ [in Stdlib.setoid_ring.Algebra_syntax]
0 [in Stdlib.NArith.BinNatDef]
0 [in Stdlib.setoid_ring.Algebra_syntax]
0 [in Stdlib.ZArith.BinIntDef]
1 [in Stdlib.NArith.BinNatDef]
1 [in Stdlib.setoid_ring.Algebra_syntax]
1 [in Stdlib.ZArith.BinIntDef]
2 [in Stdlib.NArith.BinNatDef]
2 [in Stdlib.ZArith.BinIntDef]
[ ] [in Stdlib.Vectors.VectorDef]
[ _ ; .. ; _ ] [in Stdlib.Sorting.Mergesort]
[ ] [in Stdlib.Sorting.Mergesort]
[ _ ; .. ; _ ] [in Stdlib.Sorting.PermutSetoid]
[ ] [in Stdlib.Sorting.PermutSetoid]
[ _ ] [in Stdlib.setoid_ring.Algebra_syntax]
[ _ ] [in Stdlib.rtauto.Rtauto]
[ _ ; .. ; _ ] [in Stdlib.Sorting.Sorted]
[ ] [in Stdlib.Sorting.Sorted]
λ _ .. _ , _ [in Stdlib.Unicode.Utf8_core]

Global Index

(22787 entries)

Notation Index

F

J

K

T

X

Y

_

(729 entries)

Module Index

J

X

Y

_

other

(767 entries)

Variable Index

H

J

Q

V

X

Y

_

other

(1469 entries)

Library Index

K

X

Y

_

other

(561 entries)

Lemma Index

other

(11410 entries)

Constructor Index

K

Q

Y

_

other

(526 entries)

Axiom Index

J

K

V

X

Y

_

other

(359 entries)

Inductive Index

Q

X

Y

_

other

(209 entries)

Projection Index

G

K

V

X

Y

_

other

(403 entries)

Section Index

H

J

Q

X

Y

_

other

(393 entries)

Instance Index

J

V

X

Y

_

other

(789 entries)

Abbreviation Index

J

V

Y

_

other

(1186 entries)

Definition Index

_

other

(3882 entries)

Record Index

J

K

V

X

Y

_

other

(104 entries)