Standard Library | The Coq Proof Assistant

Global Index

(22221 entries)

Notation Index

F

J

K

T

X

Y

_

(923 entries)

Module Index

J

X

Y

_

other

(744 entries)

Variable Index

H

J

Q

V

X

Y

_

other

(1480 entries)

Library Index

K

X

Y

_

other

(501 entries)

Lemma Index

other

(10364 entries)

Constructor Index

K

Y

_

other

(910 entries)

Axiom Index

K

V

X

Y

_

other

(573 entries)

Projection Index

G

K

L

V

X

Y

_

other

(386 entries)

Inductive Index

K

X

Y

_

other

(286 entries)

Section Index

H

J

Q

X

Y

_

other

(465 entries)

Instance Index

J

V

X

Y

_

other

(632 entries)

Abbreviation Index

J

V

Y

_

other

(1133 entries)

Definition Index

_

other

(3679 entries)

Record Index

J

V

X

Y

_

other

(145 entries)

other

if _ as _ return _ then _ else _ (boolean_if_scope) [notation, in Coq.ssr.ssreflect]
if _ then _ else _ (boolean_if_scope) [notation, in Coq.ssr.ssreflect]
if _ return _ then _ else _ (boolean_if_scope) [notation, in Coq.ssr.ssreflect]
_ \is an _ (bool_scope) [notation, in Coq.ssr.ssrbool]
_ \is a _ (bool_scope) [notation, in Coq.ssr.ssrbool]
_ \is _ (bool_scope) [notation, in Coq.ssr.ssrbool]
_ \in _ (bool_scope) [notation, in Coq.ssr.ssrbool]
_ \isn't an _ (bool_scope) [notation, in Coq.ssr.ssrbool]
_ \isn't a _ (bool_scope) [notation, in Coq.ssr.ssrbool]
_ \isn't _ (bool_scope) [notation, in Coq.ssr.ssrbool]
_ \is an _ (bool_scope) [notation, in Coq.ssr.ssrbool]
_ \is a _ (bool_scope) [notation, in Coq.ssr.ssrbool]
_ \is _ (bool_scope) [notation, in Coq.ssr.ssrbool]
_ \notin _ (bool_scope) [notation, in Coq.ssr.ssrbool]
_ \in _ (bool_scope) [notation, in Coq.ssr.ssrbool]
_ \in _ (bool_scope) [notation, in Coq.ssr.ssrbool]
[ ==> _ => _ ] (bool_scope) [notation, in Coq.ssr.ssrbool]
[ ==> _ , _ , .. , _ => _ ] (bool_scope) [notation, in Coq.ssr.ssrbool]
[ || _ , _ , .. , _ | _ ] (bool_scope) [notation, in Coq.ssr.ssrbool]
[ || _ | _ ] (bool_scope) [notation, in Coq.ssr.ssrbool]
[ && _ , _ , .. , _ & _ ] (bool_scope) [notation, in Coq.ssr.ssrbool]
[ && _ & _ ] (bool_scope) [notation, in Coq.ssr.ssrbool]
_ (+) _ (bool_scope) [notation, in Coq.ssr.ssrbool]
_ ==> _ (bool_scope) [notation, in Coq.ssr.ssrbool]
~~ _ (bool_scope) [notation, in Coq.ssr.ssrbool]
_ && _ (bool_scope) [notation, in Coq.Init.Datatypes]
_ || _ (bool_scope) [notation, in Coq.Init.Datatypes]
_ =? _ (char_scope) [notation, in Coq.Strings.Ascii]
_ : Prop (core_scope) [notation, in Coq.ssr.ssreflect]
_ : Type (core_scope) [notation, in Coq.ssr.ssreflect]
_ : _ (core_scope) [notation, in Coq.ssr.ssreflect]
( _ , _ , .. , _ ) (core_scope) [notation, in Coq.Init.Datatypes]
_ =~= _ (equiv_scope) [notation, in Coq.Classes.CEquivalence]
_ =/= _ (equiv_scope) [notation, in Coq.Classes.CEquivalence]
_ === _ (equiv_scope) [notation, in Coq.Classes.CEquivalence]
_ <> _ (equiv_scope) [notation, in Coq.Classes.EquivDec]
_ == _ (equiv_scope) [notation, in Coq.Classes.EquivDec]
_ =~= _ (equiv_scope) [notation, in Coq.Classes.Equivalence]
_ =/= _ (equiv_scope) [notation, in Coq.Classes.Equivalence]
_ === _ (equiv_scope) [notation, in Coq.Classes.Equivalence]
[ qualify an _ : _ | _ ] (form_scope) [notation, in Coq.ssr.ssrbool]
[ qualify an _ | _ ] (form_scope) [notation, in Coq.ssr.ssrbool]
[ qualify a _ : _ | _ ] (form_scope) [notation, in Coq.ssr.ssrbool]
[ qualify a _ | _ ] (form_scope) [notation, in Coq.ssr.ssrbool]
[ qualify _ : _ | _ ] (form_scope) [notation, in Coq.ssr.ssrbool]
[ qualify _ | _ ] (form_scope) [notation, in Coq.ssr.ssrbool]
[ predType of _ ] (form_scope) [notation, in Coq.ssr.ssrbool]
[ unlockable fun _ ] (form_scope) [notation, in Coq.ssr.ssreflect]
[ unlockable of _ ] (form_scope) [notation, in Coq.ssr.ssreflect]
=^~ _ (form_scope) [notation, in Coq.ssr.ssreflect]
[ the _ of _ ] (form_scope) [notation, in Coq.ssr.ssreflect]
[ the _ of _ by _ ] (form_scope) [notation, in Coq.ssr.ssreflect]
[ the _ of _ ] (form_scope) [notation, in Coq.ssr.ssreflect]
[ the _ of _ by _ ] (form_scope) [notation, in Coq.ssr.ssreflect]
[ rel _ _ in _ ] (fun_scope) [notation, in Coq.ssr.ssrbool]
[ rel _ _ in _ | _ ] (fun_scope) [notation, in Coq.ssr.ssrbool]
[ rel _ _ in _ & _ ] (fun_scope) [notation, in Coq.ssr.ssrbool]
[ rel _ _ in _ & _ | _ ] (fun_scope) [notation, in Coq.ssr.ssrbool]
[ pred _ in _ | _ & _ ] (fun_scope) [notation, in Coq.ssr.ssrbool]
[ pred _ in _ | _ ] (fun_scope) [notation, in Coq.ssr.ssrbool]
[ pred _ in _ ] (fun_scope) [notation, in Coq.ssr.ssrbool]
[ preim _ of _ ] (fun_scope) [notation, in Coq.ssr.ssrbool]
[ predC _ ] (fun_scope) [notation, in Coq.ssr.ssrbool]
[ predD _ & _ ] (fun_scope) [notation, in Coq.ssr.ssrbool]
[ predU _ & _ ] (fun_scope) [notation, in Coq.ssr.ssrbool]
[ predI _ & _ ] (fun_scope) [notation, in Coq.ssr.ssrbool]
[ mem _ ] (fun_scope) [notation, in Coq.ssr.ssrbool]
[ rel _ _ : _ | _ ] (fun_scope) [notation, in Coq.ssr.ssrbool]
[ rel _ _ | _ ] (fun_scope) [notation, in Coq.ssr.ssrbool]
[ pred _ : _ | _ & _ ] (fun_scope) [notation, in Coq.ssr.ssrbool]
[ pred _ : _ | _ ] (fun_scope) [notation, in Coq.ssr.ssrbool]
[ pred _ | _ & _ ] (fun_scope) [notation, in Coq.ssr.ssrbool]
[ pred _ | _ ] (fun_scope) [notation, in Coq.ssr.ssrbool]
[ pred : _ | _ ] (fun_scope) [notation, in Coq.ssr.ssrbool]
@ id _ (fun_scope) [notation, in Coq.ssr.ssrfun]
fun => _ (fun_scope) [notation, in Coq.ssr.ssrfun]
[ eta _ ] (fun_scope) [notation, in Coq.ssr.ssrfun]
_ \; _ (fun_scope) [notation, in Coq.ssr.ssrfun]
_ \o _ (fun_scope) [notation, in Coq.ssr.ssrfun]
_ =2 _ :> _ (fun_scope) [notation, in Coq.ssr.ssrfun]
_ =2 _ (fun_scope) [notation, in Coq.ssr.ssrfun]
_ =1 _ :> _ (fun_scope) [notation, in Coq.ssr.ssrfun]
_ =1 _ (fun_scope) [notation, in Coq.ssr.ssrfun]
[ fun ( _ : _ ) ( _ : _ ) => _ ] (fun_scope) [notation, in Coq.ssr.ssrfun]
[ fun _ ( _ : _ ) => _ ] (fun_scope) [notation, in Coq.ssr.ssrfun]
[ fun ( _ : _ ) _ => _ ] (fun_scope) [notation, in Coq.ssr.ssrfun]
[ fun _ _ : _ => _ ] (fun_scope) [notation, in Coq.ssr.ssrfun]
[ fun _ : _ => _ ] (fun_scope) [notation, in Coq.ssr.ssrfun]
[ fun _ _ => _ ] (fun_scope) [notation, in Coq.ssr.ssrfun]
[ fun _ => _ ] (fun_scope) [notation, in Coq.ssr.ssrfun]
[ fun : _ => _ ] (fun_scope) [notation, in Coq.ssr.ssrfun]
@^~ _ (fun_scope) [notation, in Coq.ssr.ssrfun]
_ ^~ _ (fun_scope) [notation, in Coq.ssr.ssrfun]
if _ as _ return _ then _ else _ (general_if_scope) [notation, in Coq.ssr.ssreflect]
if _ return _ then _ else _ (general_if_scope) [notation, in Coq.ssr.ssreflect]
if _ then _ else _ (general_if_scope) [notation, in Coq.ssr.ssreflect]
_ ?= _ (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]
_ ≡ _ (int63_scope) [notation, in Coq.Numbers.Cyclic.Int63.Int63]
φ _ (int63_scope) [notation, in Coq.Numbers.Cyclic.Int63.Int63]
[|| _ ||] (int63_scope) [notation, in Coq.Numbers.Cyclic.Int63.Int63]
[-| _ |] (int63_scope) [notation, in Coq.Numbers.Cyclic.Int63.Int63]
[+| _ |] (int63_scope) [notation, in Coq.Numbers.Cyclic.Int63.Int63]
[| _ |] (int63_scope) [notation, in Coq.Numbers.Cyclic.Int63.Int63]
_ ?= _ (int63_scope) [notation, in Coq.Numbers.Cyclic.Int63.Int63]
_ -c _ (int63_scope) [notation, in Coq.Numbers.Cyclic.Int63.Int63]
_ +c _ (int63_scope) [notation, in Coq.Numbers.Cyclic.Int63.Int63]
- _ (int63_scope) [notation, in Coq.Numbers.Cyclic.Int63.Int63]
_ ≤ _ (int63_scope) [notation, in Coq.Numbers.Cyclic.Int63.Int63]
_ <= _ (int63_scope) [notation, in Coq.Numbers.Cyclic.Int63.Int63]
_ < _ (int63_scope) [notation, in Coq.Numbers.Cyclic.Int63.Int63]
_ == _ (int63_scope) [notation, in Coq.Numbers.Cyclic.Int63.Int63]
_ \% _ (int63_scope) [notation, in Coq.Numbers.Cyclic.Int63.Int63]
_ / _ (int63_scope) [notation, in Coq.Numbers.Cyclic.Int63.Int63]
_ * _ (int63_scope) [notation, in Coq.Numbers.Cyclic.Int63.Int63]
_ - _ (int63_scope) [notation, in Coq.Numbers.Cyclic.Int63.Int63]
_ + _ (int63_scope) [notation, in Coq.Numbers.Cyclic.Int63.Int63]
_ lxor _ (int63_scope) [notation, in Coq.Numbers.Cyclic.Int63.Int63]
_ lor _ (int63_scope) [notation, in Coq.Numbers.Cyclic.Int63.Int63]
_ land _ (int63_scope) [notation, in Coq.Numbers.Cyclic.Int63.Int63]
_ >> _ (int63_scope) [notation, in Coq.Numbers.Cyclic.Int63.Int63]
_ << _ (int63_scope) [notation, in Coq.Numbers.Cyclic.Int63.Int63]
_ *c _ (int63_scope) [notation, in Coq.Numbers.Cyclic.Int63.Cyclic63]
_ ||| _ (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]
_ mod _ (nat_scope) [notation, in Coq.Init.Nat]
_ / _ (nat_scope) [notation, in Coq.Init.Nat]
_ ^ _ (nat_scope) [notation, in Coq.Init.Nat]
_ ?= _ (nat_scope) [notation, in Coq.Init.Nat]
_ [notation, in Coq.Init.Nat]
_ <=? _ (nat_scope) [notation, in Coq.Init.Nat]
_ =? _ (nat_scope) [notation, in Coq.Init.Nat]
_ - _ (nat_scope) [notation, in Coq.Init.Nat]
_ * _ (nat_scope) [notation, in Coq.Init.Nat]
_ + _ (nat_scope) [notation, in Coq.Init.Nat]
_ < _ <= _ (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]
_ mod _ (nat_scope) [notation, in Coq.Arith.PeanoNat]
_ / _ (nat_scope) [notation, in Coq.Arith.PeanoNat]
_ ?= _ (nat_scope) [notation, in Coq.Arith.PeanoNat]
_ [notation, in Coq.Arith.PeanoNat]
_ <=? _ (nat_scope) [notation, in Coq.Arith.PeanoNat]
_ =? _ (nat_scope) [notation, in Coq.Arith.PeanoNat]
_ ^ _ (nat_scope) [notation, in Coq.Arith.PeanoNat]
( _ | _ ) (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.ssr.ssrfun]
_ .1 (pair_scope) [notation, in Coq.ssr.ssrfun]
_ #2 (pair_scope) [notation, in Coq.FSets.FMapAVL]
_ #1 (pair_scope) [notation, in Coq.FSets.FMapAVL]
_ #2 (pair_scope) [notation, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
_ #1 (pair_scope) [notation, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
_ ~ 0 (positive_scope) [notation, in Coq.PArith.BinPosDef]
_ ~ 1 (positive_scope) [notation, in Coq.PArith.BinPosDef]
( _ | _ ) (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]
∙⊥∙ (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.Qcabs]
_ ^ _ (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]
_ # _ (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.RIneq]
_ < _ <= _ (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 _ (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]
_ (* _ *) (ssr_scope) [notation, in Coq.ssr.ssreflect]
(ssr_scope) [notation, in Coq.ssr.ssreflect]
_ ++ _ (string_scope) [notation, in Coq.Strings.String]
_ =? _ (string_scope) [notation, in Coq.Strings.String]
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]
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.Init.Logic]
_ + { _ } (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]
{ _ : _ & _ & _ } (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]
{ on _ , bijective _ } (type_scope) [notation, in Coq.ssr.ssrbool]
{ in _ , bijective _ } (type_scope) [notation, in Coq.ssr.ssrbool]
{ on _ , _ & _ } (type_scope) [notation, in Coq.ssr.ssrbool]
{ on _ & , _ } (type_scope) [notation, in Coq.ssr.ssrbool]
{ on _ , _ } (type_scope) [notation, in Coq.ssr.ssrbool]
{ in _ & & , _ } (type_scope) [notation, in Coq.ssr.ssrbool]
{ in _ & _ & , _ } (type_scope) [notation, in Coq.ssr.ssrbool]
{ in _ & & _ , _ } (type_scope) [notation, in Coq.ssr.ssrbool]
{ in _ & _ & _ , _ } (type_scope) [notation, in Coq.ssr.ssrbool]
{ in _ & , _ } (type_scope) [notation, in Coq.ssr.ssrbool]
{ in _ & _ , _ } (type_scope) [notation, in Coq.ssr.ssrbool]
{ in _ , _ } (type_scope) [notation, in Coq.ssr.ssrbool]
{ for _ , _ } (type_scope) [notation, in Coq.ssr.ssrbool]
{ subset _ <= _ } (type_scope) [notation, in Coq.ssr.ssrbool]
_ =i _ (type_scope) [notation, in Coq.ssr.ssrbool]
{ : _ } (type_scope) [notation, in Coq.ssr.ssrbool]
{ pred _ } (type_scope) [notation, in Coq.ssr.ssrbool]
[ \/ _ , _ , _ | _ ] (type_scope) [notation, in Coq.ssr.ssrbool]
[ \/ _ , _ | _ ] (type_scope) [notation, in Coq.ssr.ssrbool]
[ \/ _ | _ ] (type_scope) [notation, in Coq.ssr.ssrbool]
[ /\ _ , _ , _ , _ & _ ] (type_scope) [notation, in Coq.ssr.ssrbool]
[ /\ _ , _ , _ & _ ] (type_scope) [notation, in Coq.ssr.ssrbool]
[ /\ _ , _ & _ ] (type_scope) [notation, in Coq.ssr.ssrbool]
[ /\ _ & _ ] (type_scope) [notation, in Coq.ssr.ssrbool]
\unless _ , _ (type_scope) [notation, in Coq.ssr.ssrbool]
_ =~= _ (type_scope) [notation, in Coq.Classes.SetoidClass]
_ =/= _ (type_scope) [notation, in Coq.Classes.SetoidClass]
_ == _ (type_scope) [notation, in Coq.Classes.SetoidClass]
{ mono _ : _ _ /~ _ } (type_scope) [notation, in Coq.ssr.ssrfun]
{ mono _ : _ _ / _ } (type_scope) [notation, in Coq.ssr.ssrfun]
{ mono _ : _ _ / _ >-> _ } (type_scope) [notation, in Coq.ssr.ssrfun]
{ mono _ : _ / _ } (type_scope) [notation, in Coq.ssr.ssrfun]
{ mono _ : _ / _ >-> _ } (type_scope) [notation, in Coq.ssr.ssrfun]
{ homo _ : _ _ /~ _ } (type_scope) [notation, in Coq.ssr.ssrfun]
{ homo _ : _ _ / _ } (type_scope) [notation, in Coq.ssr.ssrfun]
{ homo _ : _ _ / _ >-> _ } (type_scope) [notation, in Coq.ssr.ssrfun]
{ homo _ : _ / _ } (type_scope) [notation, in Coq.ssr.ssrfun]
{ homo _ : _ / _ >-> _ } (type_scope) [notation, in Coq.ssr.ssrfun]
{ morph _ : _ _ / _ } (type_scope) [notation, in Coq.ssr.ssrfun]
{ morph _ : _ _ / _ >-> _ } (type_scope) [notation, in Coq.ssr.ssrfun]
{ morph _ : _ / _ } (type_scope) [notation, in Coq.ssr.ssrfun]
{ morph _ : _ / _ >-> _ } (type_scope) [notation, in Coq.ssr.ssrfun]
{ type of _ for _ } (type_scope) [notation, in Coq.ssr.ssreflect]
_ * _ (type_scope) [notation, in Coq.Init.Datatypes]
_ + _ (type_scope) [notation, in Coq.Init.Datatypes]
{ ( _ , _ ) : _ | _ } (type_scope) [notation, in Coq.Program.Utils]
_ ^ _ (type_scope) [notation, in Coq.Numbers.NaryFunctions]
_ ^^ _ --> _ (type_scope) [notation, in Coq.Numbers.NaryFunctions]
() (type_scope) [notation, in Coq.Program.Syntax]
_ ≠ _ (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]
_ ^^ _ (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]
_ ^ _ [notation, in Coq.Numbers.NatInt.NZDomain]
_ == _ [notation, in Coq.NArith.Ndigits]
_ .2 [notation, in Coq.Init.Specif]
_ .1 [notation, in Coq.Init.Specif]
_ + _ [notation, in Coq.Structures.OrdersTac]
_ =_D _ [notation, in Coq.Reals.Rtopology]
_ <>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.Unicode.Utf8]
_ ≤ _ [notation, in Coq.Unicode.Utf8]
_ ^ _ [notation, in Coq.setoid_ring.Algebra_syntax]
_ == _ [notation, in Coq.setoid_ring.Algebra_syntax]
_ - _ [notation, in Coq.setoid_ring.Algebra_syntax]
_ * _ [notation, in Coq.setoid_ring.Algebra_syntax]
_ + _ [notation, in Coq.setoid_ring.Algebra_syntax]
_ || _ [notation, in Coq.Strings.HexString]
_ :: _ [notation, in Coq.Classes.RelationClasses]
_ [@ _ ] [notation, in Coq.Vectors.VectorDef]
_ :: _ [notation, in Coq.Vectors.VectorDef]
_ ~= _ [notation, in Coq.Program.Equality]
_ \ _ [notation, in Coq.rtauto.Bintree]
_ <>b _ [notation, in Coq.Classes.EquivDec]
_ ==b _ [notation, in Coq.Classes.EquivDec]
_ \\// _ [notation, in Coq.rtauto.Rtauto]
_ //\\ _ [notation, in Coq.rtauto.Rtauto]
_ =>> _ [notation, in Coq.rtauto.Rtauto]
rew dependent _ in _ [notation, in Coq.Init.Logic]
rew dependent _ in _ [notation, in Coq.Init.Specif]
Set [notation, in Coq.Logic.SetIsType]
_==_ [notation, in Coq.setoid_ring.Algebra_syntax]
_-_ [notation, in Coq.setoid_ring.Algebra_syntax]
_*_ [notation, in Coq.setoid_ring.Algebra_syntax]
_+_ [notation, in Coq.setoid_ring.Algebra_syntax]
# [notation, in Coq.rtauto.Rtauto]
( _ ; _ ) [notation, in Coq.Init.Specif]
() [notation, in Coq.Program.Syntax]
-_ [notation, in Coq.setoid_ring.Algebra_syntax]
- _ [notation, in Coq.setoid_ring.Algebra_syntax]
0 [notation, in Coq.NArith.BinNatDef]
0 [notation, in Coq.Init.Byte]
0 [notation, in Coq.Init.Nat]
0 [notation, in Coq.ZArith.BinIntDef]
0 [notation, in Coq.setoid_ring.Algebra_syntax]
0 [notation, in Coq.Init.Peano]
1 [notation, in Coq.NArith.BinNatDef]
1 [notation, in Coq.Init.Byte]
1 [notation, in Coq.PArith.BinPosDef]
1 [notation, in Coq.Init.Nat]
1 [notation, in Coq.ZArith.BinIntDef]
1 [notation, in Coq.setoid_ring.Algebra_syntax]
2 [notation, in Coq.NArith.BinNatDef]
2 [notation, in Coq.Init.Nat]
2 [notation, in Coq.ZArith.BinIntDef]
@ sval [notation, in Coq.ssr.ssrfun]
[ _ ; .. ; _ ] [notation, in Coq.Sorting.PermutSetoid]
[ ] [notation, in Coq.Sorting.PermutSetoid]
[ _ ] [notation, in Coq.setoid_ring.Algebra_syntax]
[ _ ; .. ; _ ] [notation, in Coq.Sorting.Mergesort]
[ ] [notation, in Coq.Sorting.Mergesort]
[ ] [notation, in Coq.Vectors.VectorDef]
[ _ ; .. ; _ ] [notation, in Coq.Sorting.Sorted]
[ ] [notation, in Coq.Sorting.Sorted]
[ _ ] [notation, in Coq.rtauto.Rtauto]
{ all3 _ } [notation, in Coq.ssr.ssrbool]
{ all2 _ } [notation, in Coq.ssr.ssrbool]
{ all1 _ } [notation, in Coq.ssr.ssrbool]
λ _ .. _ , _ [notation, in Coq.Unicode.Utf8_core]

Global Index

(22221 entries)

Notation Index

F

J

K

T

X

Y

_

(923 entries)

Module Index

J

X

Y

_

other

(744 entries)

Variable Index

H

J

Q

V

X

Y

_

other

(1480 entries)

Library Index

K

X

Y

_

other

(501 entries)

Lemma Index

other

(10364 entries)

Constructor Index

K

Y

_

other

(910 entries)

Axiom Index

K

V

X

Y

_

other

(573 entries)

Projection Index

G

K

L

V

X

Y

_

other

(386 entries)

Inductive Index

K

X

Y

_

other

(286 entries)

Section Index

H

J

Q

X

Y

_

other

(465 entries)

Instance Index

J

V

X

Y

_

other

(632 entries)

Abbreviation Index

J

V

Y

_

other

(1133 entries)

Definition Index

_

other

(3679 entries)

Record Index

J

V

X

Y

_

other

(145 entries)