Standard Library | The Coq Proof Assistant

Global Index

(18818 entries)

Instance Index

G

J

V

X

Y

_

other

(548 entries)

Projection Index

G

H

K

L

V

X

Y

_

other

(206 entries)

Record Index

G

J

K

L

V

X

Y

_

other

(68 entries)

Lemma Index

Y

other

(8939 entries)

Section Index

H

J

Q

X

Y

_

other

(338 entries)

Constructor Index

K

V

Y

_

other

(422 entries)

Notation Index

F

J

K

T

U

X

Y

_

(644 entries)

Abbreviation Index

J

V

Y

_

other

(1243 entries)

Inductive Index

K

Q

V

X

Y

_

other

(209 entries)

Definition Index

J

_

other

(2935 entries)

Module Index

J

X

Y

_

other

(703 entries)

Axiom Index

K

V

X

Y

_

other

(699 entries)

Variable Index

H

J

Q

V

X

Y

_

other

(1456 entries)

Library Index

K

X

Y

_

other

(408 entries)

other

_ mod _ (bigN_scope) [notation, in Coq.Numbers.Natural.BigN.BigN]
[ _ ] (bigN_scope) [notation, in Coq.Numbers.Natural.BigN.BigN]
_ <= _ <= _ (bigN_scope) [notation, in Coq.Numbers.Natural.BigN.BigN]
_ <= _ < _ (bigN_scope) [notation, in Coq.Numbers.Natural.BigN.BigN]
_ < _ <= _ (bigN_scope) [notation, in Coq.Numbers.Natural.BigN.BigN]
_ < _ < _ (bigN_scope) [notation, in Coq.Numbers.Natural.BigN.BigN]
_ >= _ (bigN_scope) [notation, in Coq.Numbers.Natural.BigN.BigN]
_ > _ (bigN_scope) [notation, in Coq.Numbers.Natural.BigN.BigN]
_ <= _ (bigN_scope) [notation, in Coq.Numbers.Natural.BigN.BigN]
_ < _ (bigN_scope) [notation, in Coq.Numbers.Natural.BigN.BigN]
_ != _ (bigN_scope) [notation, in Coq.Numbers.Natural.BigN.BigN]
_ == _ (bigN_scope) [notation, in Coq.Numbers.Natural.BigN.BigN]
_ [notation, in Coq.Numbers.Natural.BigN.BigN]
_ <=? _ (bigN_scope) [notation, in Coq.Numbers.Natural.BigN.BigN]
_ =? _ (bigN_scope) [notation, in Coq.Numbers.Natural.BigN.BigN]
_ ?= _ (bigN_scope) [notation, in Coq.Numbers.Natural.BigN.BigN]
_ ^ _ (bigN_scope) [notation, in Coq.Numbers.Natural.BigN.BigN]
_ / _ (bigN_scope) [notation, in Coq.Numbers.Natural.BigN.BigN]
_ * _ (bigN_scope) [notation, in Coq.Numbers.Natural.BigN.BigN]
_ - _ (bigN_scope) [notation, in Coq.Numbers.Natural.BigN.BigN]
_ + _ (bigN_scope) [notation, in Coq.Numbers.Natural.BigN.BigN]
2 (bigN_scope) [notation, in Coq.Numbers.Natural.BigN.BigN]
1 (bigN_scope) [notation, in Coq.Numbers.Natural.BigN.BigN]
0 (bigN_scope) [notation, in Coq.Numbers.Natural.BigN.BigN]
[ _ ] (bigQ_scope) [notation, in Coq.Numbers.Rational.BigQ.BigQ]
_ <= _ <= _ (bigQ_scope) [notation, in Coq.Numbers.Rational.BigQ.BigQ]
_ <= _ < _ (bigQ_scope) [notation, in Coq.Numbers.Rational.BigQ.BigQ]
_ < _ <= _ (bigQ_scope) [notation, in Coq.Numbers.Rational.BigQ.BigQ]
_ < _ < _ (bigQ_scope) [notation, in Coq.Numbers.Rational.BigQ.BigQ]
_ >= _ (bigQ_scope) [notation, in Coq.Numbers.Rational.BigQ.BigQ]
_ > _ (bigQ_scope) [notation, in Coq.Numbers.Rational.BigQ.BigQ]
_ <= _ (bigQ_scope) [notation, in Coq.Numbers.Rational.BigQ.BigQ]
_ < _ (bigQ_scope) [notation, in Coq.Numbers.Rational.BigQ.BigQ]
_ != _ (bigQ_scope) [notation, in Coq.Numbers.Rational.BigQ.BigQ]
_ == _ (bigQ_scope) [notation, in Coq.Numbers.Rational.BigQ.BigQ]
_ ?= _ (bigQ_scope) [notation, in Coq.Numbers.Rational.BigQ.BigQ]
_ ^ _ (bigQ_scope) [notation, in Coq.Numbers.Rational.BigQ.BigQ]
_ / _ (bigQ_scope) [notation, in Coq.Numbers.Rational.BigQ.BigQ]
_ * _ (bigQ_scope) [notation, in Coq.Numbers.Rational.BigQ.BigQ]
- _ (bigQ_scope) [notation, in Coq.Numbers.Rational.BigQ.BigQ]
_ - _ (bigQ_scope) [notation, in Coq.Numbers.Rational.BigQ.BigQ]
_ + _ (bigQ_scope) [notation, in Coq.Numbers.Rational.BigQ.BigQ]
1 (bigQ_scope) [notation, in Coq.Numbers.Rational.BigQ.BigQ]
0 (bigQ_scope) [notation, in Coq.Numbers.Rational.BigQ.BigQ]
_ # _ (bigQ_scope) [notation, in Coq.Numbers.Rational.BigQ.BigQ]
_ ÷ _ (bigZ_scope) [notation, in Coq.Numbers.Integer.BigZ.BigZ]
_ mod _ (bigZ_scope) [notation, in Coq.Numbers.Integer.BigZ.BigZ]
[ _ ] (bigZ_scope) [notation, in Coq.Numbers.Integer.BigZ.BigZ]
_ <= _ <= _ (bigZ_scope) [notation, in Coq.Numbers.Integer.BigZ.BigZ]
_ <= _ < _ (bigZ_scope) [notation, in Coq.Numbers.Integer.BigZ.BigZ]
_ < _ <= _ (bigZ_scope) [notation, in Coq.Numbers.Integer.BigZ.BigZ]
_ < _ < _ (bigZ_scope) [notation, in Coq.Numbers.Integer.BigZ.BigZ]
_ >= _ (bigZ_scope) [notation, in Coq.Numbers.Integer.BigZ.BigZ]
_ > _ (bigZ_scope) [notation, in Coq.Numbers.Integer.BigZ.BigZ]
_ <= _ (bigZ_scope) [notation, in Coq.Numbers.Integer.BigZ.BigZ]
_ < _ (bigZ_scope) [notation, in Coq.Numbers.Integer.BigZ.BigZ]
_ != _ (bigZ_scope) [notation, in Coq.Numbers.Integer.BigZ.BigZ]
_ == _ (bigZ_scope) [notation, in Coq.Numbers.Integer.BigZ.BigZ]
_ [notation, in Coq.Numbers.Integer.BigZ.BigZ]
_ <=? _ (bigZ_scope) [notation, in Coq.Numbers.Integer.BigZ.BigZ]
_ =? _ (bigZ_scope) [notation, in Coq.Numbers.Integer.BigZ.BigZ]
_ ?= _ (bigZ_scope) [notation, in Coq.Numbers.Integer.BigZ.BigZ]
_ ^ _ (bigZ_scope) [notation, in Coq.Numbers.Integer.BigZ.BigZ]
_ / _ (bigZ_scope) [notation, in Coq.Numbers.Integer.BigZ.BigZ]
_ * _ (bigZ_scope) [notation, in Coq.Numbers.Integer.BigZ.BigZ]
- _ (bigZ_scope) [notation, in Coq.Numbers.Integer.BigZ.BigZ]
_ - _ (bigZ_scope) [notation, in Coq.Numbers.Integer.BigZ.BigZ]
_ + _ (bigZ_scope) [notation, in Coq.Numbers.Integer.BigZ.BigZ]
2 (bigZ_scope) [notation, in Coq.Numbers.Integer.BigZ.BigZ]
1 (bigZ_scope) [notation, in Coq.Numbers.Integer.BigZ.BigZ]
0 (bigZ_scope) [notation, in Coq.Numbers.Integer.BigZ.BigZ]
_ && _ (bool_scope) [notation, in Coq.Init.Datatypes]
_ || _ (bool_scope) [notation, in Coq.Init.Datatypes]
( _ , _ , .. , _ ) (core_scope) [notation, in Coq.Init.Datatypes]
_ =~= _ (equiv_scope) [notation, in Coq.Classes.Equivalence]
_ =/= _ (equiv_scope) [notation, in Coq.Classes.Equivalence]
_ === _ (equiv_scope) [notation, in Coq.Classes.Equivalence]
_ <> _ (equiv_scope) [notation, in Coq.Classes.EquivDec]
_ == _ (equiv_scope) [notation, in Coq.Classes.EquivDec]
_ ?= _ (int31_scope) [notation, in Coq.Numbers.Cyclic.Int31.Int31]
_ / _ (int31_scope) [notation, in Coq.Numbers.Cyclic.Int31.Int31]
_ *c _ (int31_scope) [notation, in Coq.Numbers.Cyclic.Int31.Int31]
_ * _ (int31_scope) [notation, in Coq.Numbers.Cyclic.Int31.Int31]
- _ (int31_scope) [notation, in Coq.Numbers.Cyclic.Int31.Int31]
_ -c _ (int31_scope) [notation, in Coq.Numbers.Cyclic.Int31.Int31]
_ - _ (int31_scope) [notation, in Coq.Numbers.Cyclic.Int31.Int31]
_ +c _ (int31_scope) [notation, in Coq.Numbers.Cyclic.Int31.Int31]
_ + _ (int31_scope) [notation, in Coq.Numbers.Cyclic.Int31.Int31]
_ ||| _ (lazy_bool_scope) [notation, in Coq.Bool.Bool]
_ &&& _ (lazy_bool_scope) [notation, in Coq.Bool.Bool]
_ ++ _ (list_scope) [notation, in Coq.Init.Datatypes]
_ :: _ (list_scope) [notation, in Coq.Init.Datatypes]
( _ | _ ) (nat_scope) [notation, in Coq.Numbers.Natural.Peano.NPeano]
_ mod _ (nat_scope) [notation, in Coq.Numbers.Natural.Peano.NPeano]
_ / _ (nat_scope) [notation, in Coq.Numbers.Natural.Peano.NPeano]
_ ^ _ (nat_scope) [notation, in Coq.Numbers.Natural.Peano.NPeano]
_ [notation, in Coq.Numbers.Natural.Peano.NPeano]
_ <=? _ (nat_scope) [notation, in Coq.Numbers.Natural.Peano.NPeano]
_ < _ <= _ (nat_scope) [notation, in Coq.Init.Peano]
_ < _ < _ (nat_scope) [notation, in Coq.Init.Peano]
_ <= _ < _ (nat_scope) [notation, in Coq.Init.Peano]
_ <= _ <= _ (nat_scope) [notation, in Coq.Init.Peano]
_ > _ (nat_scope) [notation, in Coq.Init.Peano]
_ >= _ (nat_scope) [notation, in Coq.Init.Peano]
_ < _ (nat_scope) [notation, in Coq.Init.Peano]
_ <= _ (nat_scope) [notation, in Coq.Init.Peano]
_ - _ (nat_scope) [notation, in Coq.Init.Peano]
_ * _ (nat_scope) [notation, in Coq.Init.Peano]
_ + _ (nat_scope) [notation, in Coq.Init.Peano]
( _ | _ ) (N_scope) [notation, in Coq.NArith.BinNat]
_ mod _ (N_scope) [notation, in Coq.NArith.BinNat]
_ / _ (N_scope) [notation, in Coq.NArith.BinNat]
_ [notation, in Coq.NArith.BinNat]
_ <=? _ (N_scope) [notation, in Coq.NArith.BinNat]
_ =? _ (N_scope) [notation, in Coq.NArith.BinNat]
_ < _ <= _ (N_scope) [notation, in Coq.NArith.BinNat]
_ < _ < _ (N_scope) [notation, in Coq.NArith.BinNat]
_ <= _ < _ (N_scope) [notation, in Coq.NArith.BinNat]
_ <= _ <= _ (N_scope) [notation, in Coq.NArith.BinNat]
_ > _ (N_scope) [notation, in Coq.NArith.BinNat]
_ >= _ (N_scope) [notation, in Coq.NArith.BinNat]
_ < _ (N_scope) [notation, in Coq.NArith.BinNat]
_ <= _ (N_scope) [notation, in Coq.NArith.BinNat]
_ ?= _ (N_scope) [notation, in Coq.NArith.BinNat]
_ ^ _ (N_scope) [notation, in Coq.NArith.BinNat]
_ * _ (N_scope) [notation, in Coq.NArith.BinNat]
_ - _ (N_scope) [notation, in Coq.NArith.BinNat]
_ + _ (N_scope) [notation, in Coq.NArith.BinNat]
_ #2 (pair_scope) [notation, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
_ #1 (pair_scope) [notation, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
_ #2 (pair_scope) [notation, in Coq.FSets.FMapAVL]
_ #1 (pair_scope) [notation, in Coq.FSets.FMapAVL]
( _ | _ ) (positive_scope) [notation, in Coq.PArith.BinPos]
_ < _ <= _ (positive_scope) [notation, in Coq.PArith.BinPos]
_ < _ < _ (positive_scope) [notation, in Coq.PArith.BinPos]
_ <= _ < _ (positive_scope) [notation, in Coq.PArith.BinPos]
_ <= _ <= _ (positive_scope) [notation, in Coq.PArith.BinPos]
_ > _ (positive_scope) [notation, in Coq.PArith.BinPos]
_ >= _ (positive_scope) [notation, in Coq.PArith.BinPos]
_ < _ (positive_scope) [notation, in Coq.PArith.BinPos]
_ <= _ (positive_scope) [notation, in Coq.PArith.BinPos]
_ [notation, in Coq.PArith.BinPos]
_ <=? _ (positive_scope) [notation, in Coq.PArith.BinPos]
_ =? _ (positive_scope) [notation, in Coq.PArith.BinPos]
_ ?= _ (positive_scope) [notation, in Coq.PArith.BinPos]
_ ^ _ (positive_scope) [notation, in Coq.PArith.BinPos]
_ * _ (positive_scope) [notation, in Coq.PArith.BinPos]
_ - _ (positive_scope) [notation, in Coq.PArith.BinPos]
_ + _ (positive_scope) [notation, in Coq.PArith.BinPos]
_ ~ 0 (positive_scope) [notation, in Coq.PArith.BinPosDef]
_ ~ 1 (positive_scope) [notation, in Coq.PArith.BinPosDef]
∙⊥∙ (predicate_scope) [notation, in Coq.Classes.RelationClasses]
∙⊤∙ (predicate_scope) [notation, in Coq.Classes.RelationClasses]
_ \∙/ _ (predicate_scope) [notation, in Coq.Classes.RelationClasses]
_ /∙\ _ (predicate_scope) [notation, in Coq.Classes.RelationClasses]
_ -∙> _ (predicate_scope) [notation, in Coq.Classes.RelationClasses]
_ <∙> _ (predicate_scope) [notation, in Coq.Classes.RelationClasses]
_ ∘ _ (program_scope) [notation, in Coq.Program.Basics]
_ `= _ (program_scope) [notation, in Coq.Program.Utils]
` _ (program_scope) [notation, in Coq.Program.Utils]
! (program_scope) [notation, in Coq.Program.Utils]
_ ^ _ (Qc_scope) [notation, in Coq.QArith.Qcanon]
_ / _ (Qc_scope) [notation, in Coq.QArith.Qcanon]
/ _ (Qc_scope) [notation, in Coq.QArith.Qcanon]
_ - _ (Qc_scope) [notation, in Coq.QArith.Qcanon]
- _ (Qc_scope) [notation, in Coq.QArith.Qcanon]
_ * _ (Qc_scope) [notation, in Coq.QArith.Qcanon]
_ + _ (Qc_scope) [notation, in Coq.QArith.Qcanon]
_ ?= _ (Qc_scope) [notation, in Coq.QArith.Qcanon]
_ < _ < _ (Qc_scope) [notation, in Coq.QArith.Qcanon]
_ <= _ <= _ (Qc_scope) [notation, in Coq.QArith.Qcanon]
_ >= _ (Qc_scope) [notation, in Coq.QArith.Qcanon]
_ > _ (Qc_scope) [notation, in Coq.QArith.Qcanon]
_ <= _ (Qc_scope) [notation, in Coq.QArith.Qcanon]
_ < _ (Qc_scope) [notation, in Coq.QArith.Qcanon]
1 (Qc_scope) [notation, in Coq.QArith.Qcanon]
0 (Qc_scope) [notation, in Coq.QArith.Qcanon]
!! (Qc_scope) [notation, in Coq.QArith.Qcanon]
_ ^ _ (Q_scope) [notation, in Coq.QArith.QArith_base]
_ / _ (Q_scope) [notation, in Coq.QArith.QArith_base]
/ _ (Q_scope) [notation, in Coq.QArith.QArith_base]
_ * _ (Q_scope) [notation, in Coq.QArith.QArith_base]
_ - _ (Q_scope) [notation, in Coq.QArith.QArith_base]
- _ (Q_scope) [notation, in Coq.QArith.QArith_base]
_ + _ (Q_scope) [notation, in Coq.QArith.QArith_base]
_ ?= _ (Q_scope) [notation, in Coq.QArith.QArith_base]
_ <= _ <= _ (Q_scope) [notation, in Coq.QArith.QArith_base]
_ >= _ (Q_scope) [notation, in Coq.QArith.QArith_base]
_ > _ (Q_scope) [notation, in Coq.QArith.QArith_base]
_ <= _ (Q_scope) [notation, in Coq.QArith.QArith_base]
_ < _ (Q_scope) [notation, in Coq.QArith.QArith_base]
_ == _ (Q_scope) [notation, in Coq.QArith.QArith_base]
1 (Q_scope) [notation, in Coq.QArith.QArith_base]
0 (Q_scope) [notation, in Coq.QArith.QArith_base]
_ # _ (Q_scope) [notation, in Coq.QArith.QArith_base]
/ _ (Rfun_scope) [notation, in Coq.Reals.Ranalysis1]
_ o _ (Rfun_scope) [notation, in Coq.Reals.Ranalysis1]
_ / _ (Rfun_scope) [notation, in Coq.Reals.Ranalysis1]
_ - _ (Rfun_scope) [notation, in Coq.Reals.Ranalysis1]
_ * _ (Rfun_scope) [notation, in Coq.Reals.Ranalysis1]
- _ (Rfun_scope) [notation, in Coq.Reals.Ranalysis1]
_ + _ (Rfun_scope) [notation, in Coq.Reals.Ranalysis1]
_ < _ <= _ (R_scope) [notation, in Coq.Reals.Rdefinitions]
_ < _ < _ (R_scope) [notation, in Coq.Reals.Rdefinitions]
_ <= _ < _ (R_scope) [notation, in Coq.Reals.Rdefinitions]
_ <= _ <= _ (R_scope) [notation, in Coq.Reals.Rdefinitions]
_ > _ (R_scope) [notation, in Coq.Reals.Rdefinitions]
_ >= _ (R_scope) [notation, in Coq.Reals.Rdefinitions]
_ <= _ (R_scope) [notation, in Coq.Reals.Rdefinitions]
_ / _ (R_scope) [notation, in Coq.Reals.Rdefinitions]
_ - _ (R_scope) [notation, in Coq.Reals.Rdefinitions]
_ < _ (R_scope) [notation, in Coq.Reals.Rdefinitions]
/ _ (R_scope) [notation, in Coq.Reals.Rdefinitions]
- _ (R_scope) [notation, in Coq.Reals.Rdefinitions]
_ * _ (R_scope) [notation, in Coq.Reals.Rdefinitions]
_ + _ (R_scope) [notation, in Coq.Reals.Rdefinitions]
_ ^Z _ (R_scope) [notation, in Coq.Reals.Rfunctions]
_ ^ _ (R_scope) [notation, in Coq.Reals.Rfunctions]
_ ² (R_scope) [notation, in Coq.Reals.RIneq]
_ ^R _ (R_scope) [notation, in Coq.Reals.Rpower]
_ * _ (signature_scope) [notation, in Coq.Classes.RelationPairs]
_ @@2 (signature_scope) [notation, in Coq.Classes.RelationPairs]
_ @@1 (signature_scope) [notation, in Coq.Classes.RelationPairs]
_ @@ _ (signature_scope) [notation, in Coq.Classes.RelationPairs]
_ ++ _ (string_scope) [notation, in Coq.Strings.String]
_ * _ (type_scope) [notation, in Coq.Init.Datatypes]
_ + _ (type_scope) [notation, in Coq.Init.Datatypes]
() (type_scope) [notation, in Coq.Program.Syntax]
_ =~= _ (type_scope) [notation, in Coq.Classes.SetoidClass]
_ =/= _ (type_scope) [notation, in Coq.Classes.SetoidClass]
_ == _ (type_scope) [notation, in Coq.Classes.SetoidClass]
_ + { _ } (type_scope) [notation, in Coq.Init.Specif]
{ _ } + { _ } (type_scope) [notation, in Coq.Init.Specif]
{ _ : _ & _ & _ } (type_scope) [notation, in Coq.Init.Specif]
{ _ : _ & _ } (type_scope) [notation, in Coq.Init.Specif]
{ _ : _ | _ & _ } (type_scope) [notation, in Coq.Init.Specif]
{ _ : _ | _ } (type_scope) [notation, in Coq.Init.Specif]
{ _ | _ & _ } (type_scope) [notation, in Coq.Init.Specif]
{ _ | _ } (type_scope) [notation, in Coq.Init.Specif]
exists ! _ .. _ , _ (type_scope) [notation, in Coq.Init.Logic]
_ <> _ (type_scope) [notation, in Coq.Init.Logic]
_ <> _ :> _ (type_scope) [notation, in Coq.Init.Logic]
_ = _ (type_scope) [notation, in Coq.Init.Logic]
_ = _ :> _ (type_scope) [notation, in Coq.Init.Logic]
exists2 _ : _ , _ & _ (type_scope) [notation, in Coq.Init.Logic]
exists2 _ , _ & _ (type_scope) [notation, in Coq.Init.Logic]
exists _ .. _ , _ (type_scope) [notation, in Coq.Init.Logic]
IF _ then _ else _ (type_scope) [notation, in Coq.Init.Logic]
_ <-> _ (type_scope) [notation, in Coq.Init.Logic]
_ \/ _ (type_scope) [notation, in Coq.Init.Logic]
_ /\ _ (type_scope) [notation, in Coq.Init.Logic]
~ _ (type_scope) [notation, in Coq.Init.Logic]
_ ≠ _ (type_scope) [notation, in Coq.Unicode.Utf8_core]
¬ _ (type_scope) [notation, in Coq.Unicode.Utf8_core]
_ ↔ _ (type_scope) [notation, in Coq.Unicode.Utf8_core]
_ → _ (type_scope) [notation, in Coq.Unicode.Utf8_core]
_ ∧ _ (type_scope) [notation, in Coq.Unicode.Utf8_core]
_ ∨ _ (type_scope) [notation, in Coq.Unicode.Utf8_core]
∃ _ .. _ , _ (type_scope) [notation, in Coq.Unicode.Utf8_core]
∀ _ .. _ , _ (type_scope) [notation, in Coq.Unicode.Utf8_core]
_ ^ _ (type_scope) [notation, in Coq.Numbers.NaryFunctions]
_ ^^ _ --> _ (type_scope) [notation, in Coq.Numbers.NaryFunctions]
{ ( _ , _ ) : _ | _ } (type_scope) [notation, in Coq.Program.Utils]
_ ^^ _ (Z_scope) [notation, in Coq.ZArith.Zpow_alt]
_ < _ <= _ (Z_scope) [notation, in Coq.ZArith.BinInt]
_ < _ < _ (Z_scope) [notation, in Coq.ZArith.BinInt]
_ <= _ < _ (Z_scope) [notation, in Coq.ZArith.BinInt]
_ <= _ <= _ (Z_scope) [notation, in Coq.ZArith.BinInt]
_ > _ (Z_scope) [notation, in Coq.ZArith.BinInt]
_ >= _ (Z_scope) [notation, in Coq.ZArith.BinInt]
_ < _ (Z_scope) [notation, in Coq.ZArith.BinInt]
_ <= _ (Z_scope) [notation, in Coq.ZArith.BinInt]
( _ | _ ) (Z_scope) [notation, in Coq.ZArith.BinInt]
_ >? _ (Z_scope) [notation, in Coq.ZArith.BinInt]
_ >=? _ (Z_scope) [notation, in Coq.ZArith.BinInt]
_ [notation, in Coq.ZArith.BinInt]
_ <=? _ (Z_scope) [notation, in Coq.ZArith.BinInt]
_ =? _ (Z_scope) [notation, in Coq.ZArith.BinInt]
_ ?= _ (Z_scope) [notation, in Coq.ZArith.BinInt]
_ ÷ _ (Z_scope) [notation, in Coq.ZArith.BinInt]
_ mod _ (Z_scope) [notation, in Coq.ZArith.BinInt]
_ / _ (Z_scope) [notation, in Coq.ZArith.BinInt]
_ ^ _ (Z_scope) [notation, in Coq.ZArith.BinInt]
_ * _ (Z_scope) [notation, in Coq.ZArith.BinInt]
_ - _ (Z_scope) [notation, in Coq.ZArith.BinInt]
- _ (Z_scope) [notation, in Coq.ZArith.BinInt]
_ + _ (Z_scope) [notation, in Coq.ZArith.BinInt]
' _ (Z_scope) [notation, in Coq.QArith.QArith_base]
_ + _ [notation, in Coq.Structures.OrdersTac]
_ << _ [notation, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleBase]
_ ≥ _ [notation, in Coq.Unicode.Utf8]
_ ≤ _ [notation, in Coq.Unicode.Utf8]
_ [@ _ ] [notation, in Coq.Vectors.VectorDef]
_ :: _ [notation, in Coq.Vectors.VectorDef]
_ ^ _ [notation, in Coq.Numbers.NatInt.NZDomain]
_ <>b _ [notation, in Coq.Classes.SetoidDec]
_ ==b _ [notation, in Coq.Classes.SetoidDec]
_ =/= _ [notation, in Coq.Classes.SetoidDec]
_ == _ [notation, in Coq.Classes.SetoidDec]
_ :: _ [notation, in Coq.Classes.RelationClasses]
_ ~= _ [notation, in Coq.Program.Equality]
_ <>b _ [notation, in Coq.Classes.EquivDec]
_ ==b _ [notation, in Coq.Classes.EquivDec]
_ == _ [notation, in Coq.NArith.Ndigits]
_ =_D _ [notation, in Coq.Reals.Rtopology]
_ << _ [notation, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleDivn1]
Set [notation, in Coq.Logic.SetIsType]
() [notation, in Coq.Program.Syntax]
[ _ ; .. ; _ ] [notation, in Coq.Sorting.PermutSetoid]
[ ] [notation, in Coq.Sorting.PermutSetoid]
[ _ ; .. ; _ ] [notation, in Coq.Sorting.Permutation]
[ ] [notation, in Coq.Sorting.Permutation]
[ _ ; .. ; _ ] [notation, in Coq.Sorting.Mergesort]
[ ] [notation, in Coq.Sorting.Mergesort]
[ _ ; .. ; _ ] [notation, in Coq.Sorting.Sorted]
[ ] [notation, in Coq.Sorting.Sorted]
[] [notation, in Coq.Vectors.VectorDef]
λ _ .. _ , _ [notation, in Coq.Unicode.Utf8_core]

Global Index

(18818 entries)

Instance Index

G

J

V

X

Y

_

other

(548 entries)

Projection Index

G

H

K

L

V

X

Y

_

other

(206 entries)

Record Index

G

J

K

L

V

X

Y

_

other

(68 entries)

Lemma Index

Y

other

(8939 entries)

Section Index

H

J

Q

X

Y

_

other

(338 entries)

Constructor Index

K

V

Y

_

other

(422 entries)

Notation Index

F

J

K

T

U

X

Y

_

(644 entries)

Abbreviation Index

J

V

Y

_

other

(1243 entries)

Inductive Index

K

Q

V

X

Y

_

other

(209 entries)

Definition Index

J

_

other

(2935 entries)

Module Index

J

X

Y

_

other

(703 entries)

Axiom Index

K

V

X

Y

_

other

(699 entries)

Variable Index

H

J

Q

V

X

Y

_

other

(1456 entries)

Library Index

K

X

Y

_

other

(408 entries)