Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (21445 entries)
Notation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (889 entries)
Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (714 entries)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1464 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (482 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (10031 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (663 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (537 entries)
Projection Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (374 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (285 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (457 entries)
Instance Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (616 entries)
Abbreviation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1328 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (3468 entries)
Record Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (137 entries)

other (notation)

if _ as _ return _ then _ else _ (boolean_if_scope) [in Coq.ssr.ssreflect]
if _ then _ else _ (boolean_if_scope) [in Coq.ssr.ssreflect]
if _ return _ then _ else _ (boolean_if_scope) [in Coq.ssr.ssreflect]
_ \i s an _ (bool_scope) [in Coq.ssr.ssrbool]
_ \i s a _ (bool_scope) [in Coq.ssr.ssrbool]
_ \i s _ (bool_scope) [in Coq.ssr.ssrbool]
_ \i n _ (bool_scope) [in Coq.ssr.ssrbool]
_ \isn't an _ (bool_scope) [in Coq.ssr.ssrbool]
_ \isn't a _ (bool_scope) [in Coq.ssr.ssrbool]
_ \isn't _ (bool_scope) [in Coq.ssr.ssrbool]
_ \is an _ (bool_scope) [in Coq.ssr.ssrbool]
_ \is a _ (bool_scope) [in Coq.ssr.ssrbool]
_ \is _ (bool_scope) [in Coq.ssr.ssrbool]
_ \notin _ (bool_scope) [in Coq.ssr.ssrbool]
_ \in _ (bool_scope) [in Coq.ssr.ssrbool]
_ \in _ (bool_scope) [in Coq.ssr.ssrbool]
[ ==> _ => _ ] (bool_scope) [in Coq.ssr.ssrbool]
[ ==> _ , _ , .. , _ => _ ] (bool_scope) [in Coq.ssr.ssrbool]
[ || _ , _ , .. , _ | _ ] (bool_scope) [in Coq.ssr.ssrbool]
[ || _ | _ ] (bool_scope) [in Coq.ssr.ssrbool]
[ && _ , _ , .. , _ & _ ] (bool_scope) [in Coq.ssr.ssrbool]
[ && _ & _ ] (bool_scope) [in Coq.ssr.ssrbool]
_ (+) _ (bool_scope) [in Coq.ssr.ssrbool]
_ ==> _ (bool_scope) [in Coq.ssr.ssrbool]
~~ _ (bool_scope) [in Coq.ssr.ssrbool]
_ && _ (bool_scope) [in Coq.Init.Datatypes]
_ || _ (bool_scope) [in Coq.Init.Datatypes]
_ : Prop (core_scope) [in Coq.ssr.ssreflect]
_ : Type (core_scope) [in Coq.ssr.ssreflect]
_ : _ (core_scope) [in Coq.ssr.ssreflect]
( _ , _ , .. , _ ) (core_scope) [in Coq.Init.Datatypes]
_ =~= _ (equiv_scope) [in Coq.Classes.CEquivalence]
_ =/= _ (equiv_scope) [in Coq.Classes.CEquivalence]
_ === _ (equiv_scope) [in Coq.Classes.CEquivalence]
_ <> _ (equiv_scope) [in Coq.Classes.EquivDec]
_ == _ (equiv_scope) [in Coq.Classes.EquivDec]
_ =~= _ (equiv_scope) [in Coq.Classes.Equivalence]
_ =/= _ (equiv_scope) [in Coq.Classes.Equivalence]
_ === _ (equiv_scope) [in Coq.Classes.Equivalence]
[ qualify an _ : _ | _ ] (form_scope) [in Coq.ssr.ssrbool]
[ qualify an _ | _ ] (form_scope) [in Coq.ssr.ssrbool]
[ qualify a _ : _ | _ ] (form_scope) [in Coq.ssr.ssrbool]
[ qualify a _ | _ ] (form_scope) [in Coq.ssr.ssrbool]
[ qualify _ : _ | _ ] (form_scope) [in Coq.ssr.ssrbool]
[ qualify _ | _ ] (form_scope) [in Coq.ssr.ssrbool]
[ predType of _ ] (form_scope) [in Coq.ssr.ssrbool]
[ unlockable fun _ ] (form_scope) [in Coq.ssr.ssreflect]
[ unlockable of _ ] (form_scope) [in Coq.ssr.ssreflect]
=^~ _ (form_scope) [in Coq.ssr.ssreflect]
[ th e _ of _ ] (form_scope) [in Coq.ssr.ssreflect]
[ th e _ of _ by _ ] (form_scope) [in Coq.ssr.ssreflect]
[ the _ of _ ] (form_scope) [in Coq.ssr.ssreflect]
[ the _ of _ by _ ] (form_scope) [in Coq.ssr.ssreflect]
[ rel _ _ in _ ] (fun_scope) [in Coq.ssr.ssrbool]
[ rel _ _ in _ | _ ] (fun_scope) [in Coq.ssr.ssrbool]
[ rel _ _ in _ & _ ] (fun_scope) [in Coq.ssr.ssrbool]
[ rel _ _ in _ & _ | _ ] (fun_scope) [in Coq.ssr.ssrbool]
[ pred _ in _ | _ & _ ] (fun_scope) [in Coq.ssr.ssrbool]
[ pred _ in _ | _ ] (fun_scope) [in Coq.ssr.ssrbool]
[ pred _ in _ ] (fun_scope) [in Coq.ssr.ssrbool]
[ preim _ of _ ] (fun_scope) [in Coq.ssr.ssrbool]
[ predC _ ] (fun_scope) [in Coq.ssr.ssrbool]
[ predD _ & _ ] (fun_scope) [in Coq.ssr.ssrbool]
[ predU _ & _ ] (fun_scope) [in Coq.ssr.ssrbool]
[ predI _ & _ ] (fun_scope) [in Coq.ssr.ssrbool]
[ rel of _ ] (fun_scope) [in Coq.ssr.ssrbool]
[ mem _ ] (fun_scope) [in Coq.ssr.ssrbool]
[ rel _ _ : _ | _ ] (fun_scope) [in Coq.ssr.ssrbool]
[ rel _ _ | _ ] (fun_scope) [in Coq.ssr.ssrbool]
[ pred _ : _ | _ & _ ] (fun_scope) [in Coq.ssr.ssrbool]
[ pred _ : _ | _ ] (fun_scope) [in Coq.ssr.ssrbool]
[ pred _ | _ & _ ] (fun_scope) [in Coq.ssr.ssrbool]
[ pred _ | _ ] (fun_scope) [in Coq.ssr.ssrbool]
[ pred : _ | _ ] (fun_scope) [in Coq.ssr.ssrbool]
@ idfun _ (fun_scope) [in Coq.ssr.ssrfun]
@ id _ (fun_scope) [in Coq.ssr.ssrfun]
fun => _ (fun_scope) [in Coq.ssr.ssrfun]
[ eta _ ] (fun_scope) [in Coq.ssr.ssrfun]
_ \; _ (fun_scope) [in Coq.ssr.ssrfun]
_ \o _ (fun_scope) [in Coq.ssr.ssrfun]
_ =2 _ :> _ (fun_scope) [in Coq.ssr.ssrfun]
_ =2 _ (fun_scope) [in Coq.ssr.ssrfun]
_ =1 _ :> _ (fun_scope) [in Coq.ssr.ssrfun]
_ =1 _ (fun_scope) [in Coq.ssr.ssrfun]
[ fun ( _ : _ ) ( _ : _ ) => _ ] (fun_scope) [in Coq.ssr.ssrfun]
[ fun _ ( _ : _ ) => _ ] (fun_scope) [in Coq.ssr.ssrfun]
[ fun ( _ : _ ) _ => _ ] (fun_scope) [in Coq.ssr.ssrfun]
[ fun _ _ : _ => _ ] (fun_scope) [in Coq.ssr.ssrfun]
[ fun _ _ => _ ] (fun_scope) [in Coq.ssr.ssrfun]
[ fun _ : _ => _ ] (fun_scope) [in Coq.ssr.ssrfun]
[ fun _ => _ ] (fun_scope) [in Coq.ssr.ssrfun]
[ fun : _ => _ ] (fun_scope) [in Coq.ssr.ssrfun]
@^~ _ (fun_scope) [in Coq.ssr.ssrfun]
_ ^~ _ (fun_scope) [in Coq.ssr.ssrfun]
if _ as _ return _ then _ else _ (general_if_scope) [in Coq.ssr.ssreflect]
if _ return _ then _ else _ (general_if_scope) [in Coq.ssr.ssreflect]
if _ then _ else _ (general_if_scope) [in Coq.ssr.ssreflect]
_ ?= _ (int31_scope) [in Coq.Numbers.Cyclic.Int31.Int31]
_ / _ (int31_scope) [in Coq.Numbers.Cyclic.Int31.Int31]
_ *c _ (int31_scope) [in Coq.Numbers.Cyclic.Int31.Int31]
_ * _ (int31_scope) [in Coq.Numbers.Cyclic.Int31.Int31]
- _ (int31_scope) [in Coq.Numbers.Cyclic.Int31.Int31]
_ -c _ (int31_scope) [in Coq.Numbers.Cyclic.Int31.Int31]
_ - _ (int31_scope) [in Coq.Numbers.Cyclic.Int31.Int31]
_ +c _ (int31_scope) [in Coq.Numbers.Cyclic.Int31.Int31]
_ + _ (int31_scope) [in Coq.Numbers.Cyclic.Int31.Int31]
_ ||| _ (lazy_bool_scope) [in Coq.Bool.Bool]
_ &&& _ (lazy_bool_scope) [in Coq.Bool.Bool]
_ ++ _ (list_scope) [in Coq.Init.Datatypes]
_ :: _ (list_scope) [in Coq.Init.Datatypes]
( _ | _ ) (nat_scope) [in Coq.Numbers.Natural.Peano.NPeano]
_ mod _ (nat_scope) [in Coq.Numbers.Natural.Peano.NPeano]
_ / _ (nat_scope) [in Coq.Numbers.Natural.Peano.NPeano]
_ ^ _ (nat_scope) [in Coq.Numbers.Natural.Peano.NPeano]
_ [in Coq.Numbers.Natural.Peano.NPeano]
_ <=? _ (nat_scope) [in Coq.Numbers.Natural.Peano.NPeano]
_ mod _ (nat_scope) [in Coq.Init.Nat]
_ / _ (nat_scope) [in Coq.Init.Nat]
_ ^ _ (nat_scope) [in Coq.Init.Nat]
_ ?= _ (nat_scope) [in Coq.Init.Nat]
_ [in Coq.Init.Nat]
_ <=? _ (nat_scope) [in Coq.Init.Nat]
_ =? _ (nat_scope) [in Coq.Init.Nat]
_ - _ (nat_scope) [in Coq.Init.Nat]
_ * _ (nat_scope) [in Coq.Init.Nat]
_ + _ (nat_scope) [in Coq.Init.Nat]
_ < _ <= _ (nat_scope) [in Coq.Init.Peano]
_ < _ < _ (nat_scope) [in Coq.Init.Peano]
_ <= _ < _ (nat_scope) [in Coq.Init.Peano]
_ <= _ <= _ (nat_scope) [in Coq.Init.Peano]
_ > _ (nat_scope) [in Coq.Init.Peano]
_ >= _ (nat_scope) [in Coq.Init.Peano]
_ < _ (nat_scope) [in Coq.Init.Peano]
_ <= _ (nat_scope) [in Coq.Init.Peano]
_ - _ (nat_scope) [in Coq.Init.Peano]
_ * _ (nat_scope) [in Coq.Init.Peano]
_ + _ (nat_scope) [in Coq.Init.Peano]
_ mod _ (nat_scope) [in Coq.Arith.PeanoNat]
_ / _ (nat_scope) [in Coq.Arith.PeanoNat]
_ ?= _ (nat_scope) [in Coq.Arith.PeanoNat]
_ [in Coq.Arith.PeanoNat]
_ <=? _ (nat_scope) [in Coq.Arith.PeanoNat]
_ =? _ (nat_scope) [in Coq.Arith.PeanoNat]
_ ^ _ (nat_scope) [in Coq.Arith.PeanoNat]
( _ | _ ) (N_scope) [in Coq.NArith.BinNat]
_ mod _ (N_scope) [in Coq.NArith.BinNat]
_ / _ (N_scope) [in Coq.NArith.BinNat]
_ [in Coq.NArith.BinNat]
_ <=? _ (N_scope) [in Coq.NArith.BinNat]
_ =? _ (N_scope) [in Coq.NArith.BinNat]
_ < _ <= _ (N_scope) [in Coq.NArith.BinNat]
_ < _ < _ (N_scope) [in Coq.NArith.BinNat]
_ <= _ < _ (N_scope) [in Coq.NArith.BinNat]
_ <= _ <= _ (N_scope) [in Coq.NArith.BinNat]
_ > _ (N_scope) [in Coq.NArith.BinNat]
_ >= _ (N_scope) [in Coq.NArith.BinNat]
_ < _ (N_scope) [in Coq.NArith.BinNat]
_ <= _ (N_scope) [in Coq.NArith.BinNat]
_ ?= _ (N_scope) [in Coq.NArith.BinNat]
_ ^ _ (N_scope) [in Coq.NArith.BinNat]
_ * _ (N_scope) [in Coq.NArith.BinNat]
_ - _ (N_scope) [in Coq.NArith.BinNat]
_ + _ (N_scope) [in Coq.NArith.BinNat]
_ .2 (pair_scope) [in Coq.ssr.ssrfun]
_ .1 (pair_scope) [in Coq.ssr.ssrfun]
_ #2 (pair_scope) [in Coq.FSets.FMapAVL]
_ #1 (pair_scope) [in Coq.FSets.FMapAVL]
_ #2 (pair_scope) [in Coq.Numbers.Integer.NatPairs.ZNatPairs]
_ #1 (pair_scope) [in Coq.Numbers.Integer.NatPairs.ZNatPairs]
_ ~ 0 (positive_scope) [in Coq.PArith.BinPosDef]
_ ~ 1 (positive_scope) [in Coq.PArith.BinPosDef]
( _ | _ ) (positive_scope) [in Coq.PArith.BinPos]
_ < _ <= _ (positive_scope) [in Coq.PArith.BinPos]
_ < _ < _ (positive_scope) [in Coq.PArith.BinPos]
_ <= _ < _ (positive_scope) [in Coq.PArith.BinPos]
_ <= _ <= _ (positive_scope) [in Coq.PArith.BinPos]
_ > _ (positive_scope) [in Coq.PArith.BinPos]
_ >= _ (positive_scope) [in Coq.PArith.BinPos]
_ < _ (positive_scope) [in Coq.PArith.BinPos]
_ <= _ (positive_scope) [in Coq.PArith.BinPos]
_ [in Coq.PArith.BinPos]
_ <=? _ (positive_scope) [in Coq.PArith.BinPos]
_ =? _ (positive_scope) [in Coq.PArith.BinPos]
_ ?= _ (positive_scope) [in Coq.PArith.BinPos]
_ ^ _ (positive_scope) [in Coq.PArith.BinPos]
_ * _ (positive_scope) [in Coq.PArith.BinPos]
_ - _ (positive_scope) [in Coq.PArith.BinPos]
_ + _ (positive_scope) [in Coq.PArith.BinPos]
∙⊥∙ (predicate_scope) [in Coq.Classes.RelationClasses]
∙⊤∙ (predicate_scope) [in Coq.Classes.RelationClasses]
_ \∙/ _ (predicate_scope) [in Coq.Classes.RelationClasses]
_ /∙\ _ (predicate_scope) [in Coq.Classes.RelationClasses]
_ -∙> _ (predicate_scope) [in Coq.Classes.RelationClasses]
_ <∙> _ (predicate_scope) [in Coq.Classes.RelationClasses]
_ ∘ _ (program_scope) [in Coq.Program.Basics]
_ `= _ (program_scope) [in Coq.Program.Utils]
` _ (program_scope) [in Coq.Program.Utils]
! (program_scope) [in Coq.Program.Utils]
_ ^ _ (Qc_scope) [in Coq.QArith.Qcanon]
_ / _ (Qc_scope) [in Coq.QArith.Qcanon]
/ _ (Qc_scope) [in Coq.QArith.Qcanon]
_ - _ (Qc_scope) [in Coq.QArith.Qcanon]
- _ (Qc_scope) [in Coq.QArith.Qcanon]
_ * _ (Qc_scope) [in Coq.QArith.Qcanon]
_ + _ (Qc_scope) [in Coq.QArith.Qcanon]
_ ?= _ (Qc_scope) [in Coq.QArith.Qcanon]
_ < _ < _ (Qc_scope) [in Coq.QArith.Qcanon]
_ <= _ <= _ (Qc_scope) [in Coq.QArith.Qcanon]
_ >= _ (Qc_scope) [in Coq.QArith.Qcanon]
_ > _ (Qc_scope) [in Coq.QArith.Qcanon]
_ <= _ (Qc_scope) [in Coq.QArith.Qcanon]
_ < _ (Qc_scope) [in Coq.QArith.Qcanon]
1 (Qc_scope) [in Coq.QArith.Qcanon]
0 (Qc_scope) [in Coq.QArith.Qcanon]
[ _ ] (Qc_scope) [in Coq.QArith.Qcabs]
_ ^ _ (Q_scope) [in Coq.QArith.QArith_base]
_ / _ (Q_scope) [in Coq.QArith.QArith_base]
/ _ (Q_scope) [in Coq.QArith.QArith_base]
_ * _ (Q_scope) [in Coq.QArith.QArith_base]
_ - _ (Q_scope) [in Coq.QArith.QArith_base]
- _ (Q_scope) [in Coq.QArith.QArith_base]
_ + _ (Q_scope) [in Coq.QArith.QArith_base]
_ ?= _ (Q_scope) [in Coq.QArith.QArith_base]
_ <= _ <= _ (Q_scope) [in Coq.QArith.QArith_base]
_ >= _ (Q_scope) [in Coq.QArith.QArith_base]
_ > _ (Q_scope) [in Coq.QArith.QArith_base]
_ <= _ (Q_scope) [in Coq.QArith.QArith_base]
_ < _ (Q_scope) [in Coq.QArith.QArith_base]
_ == _ (Q_scope) [in Coq.QArith.QArith_base]
1 (Q_scope) [in Coq.QArith.QArith_base]
0 (Q_scope) [in Coq.QArith.QArith_base]
_ # _ (Q_scope) [in Coq.QArith.QArith_base]
/ _ (Rfun_scope) [in Coq.Reals.Ranalysis1]
_ o _ (Rfun_scope) [in Coq.Reals.Ranalysis1]
_ / _ (Rfun_scope) [in Coq.Reals.Ranalysis1]
_ - _ (Rfun_scope) [in Coq.Reals.Ranalysis1]
_ * _ (Rfun_scope) [in Coq.Reals.Ranalysis1]
- _ (Rfun_scope) [in Coq.Reals.Ranalysis1]
_ + _ (Rfun_scope) [in Coq.Reals.Ranalysis1]
_ ² (R_scope) [in Coq.Reals.RIneq]
_ < _ <= _ (R_scope) [in Coq.Reals.Rdefinitions]
_ < _ < _ (R_scope) [in Coq.Reals.Rdefinitions]
_ <= _ < _ (R_scope) [in Coq.Reals.Rdefinitions]
_ <= _ <= _ (R_scope) [in Coq.Reals.Rdefinitions]
_ > _ (R_scope) [in Coq.Reals.Rdefinitions]
_ >= _ (R_scope) [in Coq.Reals.Rdefinitions]
_ <= _ (R_scope) [in Coq.Reals.Rdefinitions]
_ / _ (R_scope) [in Coq.Reals.Rdefinitions]
_ - _ (R_scope) [in Coq.Reals.Rdefinitions]
_ < _ (R_scope) [in Coq.Reals.Rdefinitions]
/ _ (R_scope) [in Coq.Reals.Rdefinitions]
- _ (R_scope) [in Coq.Reals.Rdefinitions]
_ * _ (R_scope) [in Coq.Reals.Rdefinitions]
_ + _ (R_scope) [in Coq.Reals.Rdefinitions]
_ ^Z _ (R_scope) [in Coq.Reals.Rfunctions]
_ ^ _ (R_scope) [in Coq.Reals.Rfunctions]
_ ^R _ (R_scope) [in Coq.Reals.Rpower]
_ * _ (signature_scope) [in Coq.Classes.RelationPairs]
_ @@2 (signature_scope) [in Coq.Classes.RelationPairs]
_ @@1 (signature_scope) [in Coq.Classes.RelationPairs]
_ @@ _ (signature_scope) [in Coq.Classes.RelationPairs]
_ ++ _ (string_scope) [in Coq.Strings.String]
exists ! _ .. _ , _ (type_scope) [in Coq.Init.Logic]
_ <> _ (type_scope) [in Coq.Init.Logic]
_ <> _ :> _ (type_scope) [in Coq.Init.Logic]
_ = _ (type_scope) [in Coq.Init.Logic]
_ = _ :> _ (type_scope) [in Coq.Init.Logic]
exists2 _ : _ , _ & _ (type_scope) [in Coq.Init.Logic]
exists2 _ , _ & _ (type_scope) [in Coq.Init.Logic]
exists _ .. _ , _ (type_scope) [in Coq.Init.Logic]
IF _ then _ else _ (type_scope) [in Coq.Init.Logic]
_ <-> _ (type_scope) [in Coq.Init.Logic]
_ \/ _ (type_scope) [in Coq.Init.Logic]
_ /\ _ (type_scope) [in Coq.Init.Logic]
~ _ (type_scope) [in Coq.Init.Logic]
_ -> _ (type_scope) [in Coq.Init.Logic]
_ + { _ } (type_scope) [in Coq.Init.Specif]
{ _ } + { _ } (type_scope) [in Coq.Init.Specif]
{ _ : _ & _ & _ } (type_scope) [in Coq.Init.Specif]
{ _ : _ & _ } (type_scope) [in Coq.Init.Specif]
{ _ : _ | _ & _ } (type_scope) [in Coq.Init.Specif]
{ _ : _ | _ } (type_scope) [in Coq.Init.Specif]
{ _ | _ & _ } (type_scope) [in Coq.Init.Specif]
{ _ | _ } (type_scope) [in Coq.Init.Specif]
{ on _ , bijective _ } (type_scope) [in Coq.ssr.ssrbool]
{ in _ , bijective _ } (type_scope) [in Coq.ssr.ssrbool]
{ on _ , _ & _ } (type_scope) [in Coq.ssr.ssrbool]
{ on _ & , _ } (type_scope) [in Coq.ssr.ssrbool]
{ on _ , _ } (type_scope) [in Coq.ssr.ssrbool]
{ in _ & & , _ } (type_scope) [in Coq.ssr.ssrbool]
{ in _ & _ & , _ } (type_scope) [in Coq.ssr.ssrbool]
{ in _ & & _ , _ } (type_scope) [in Coq.ssr.ssrbool]
{ in _ & _ & _ , _ } (type_scope) [in Coq.ssr.ssrbool]
{ in _ & , _ } (type_scope) [in Coq.ssr.ssrbool]
{ in _ & _ , _ } (type_scope) [in Coq.ssr.ssrbool]
{ in _ , _ } (type_scope) [in Coq.ssr.ssrbool]
{ for _ , _ } (type_scope) [in Coq.ssr.ssrbool]
{ subset _ <= _ } (type_scope) [in Coq.ssr.ssrbool]
_ =i _ (type_scope) [in Coq.ssr.ssrbool]
{ : _ } (type_scope) [in Coq.ssr.ssrbool]
[ \/ _ , _ , _ | _ ] (type_scope) [in Coq.ssr.ssrbool]
[ \/ _ , _ | _ ] (type_scope) [in Coq.ssr.ssrbool]
[ \/ _ | _ ] (type_scope) [in Coq.ssr.ssrbool]
[ /\ _ , _ , _ , _ & _ ] (type_scope) [in Coq.ssr.ssrbool]
[ /\ _ , _ , _ & _ ] (type_scope) [in Coq.ssr.ssrbool]
[ /\ _ , _ & _ ] (type_scope) [in Coq.ssr.ssrbool]
[ /\ _ & _ ] (type_scope) [in Coq.ssr.ssrbool]
\unless _ , _ (type_scope) [in Coq.ssr.ssrbool]
_ =~= _ (type_scope) [in Coq.Classes.SetoidClass]
_ =/= _ (type_scope) [in Coq.Classes.SetoidClass]
_ == _ (type_scope) [in Coq.Classes.SetoidClass]
{ mono _ : _ _ /~ _ } (type_scope) [in Coq.ssr.ssrfun]
{ mono _ : _ _ / _ } (type_scope) [in Coq.ssr.ssrfun]
{ mono _ : _ _ / _ >-> _ } (type_scope) [in Coq.ssr.ssrfun]
{ mono _ : _ / _ } (type_scope) [in Coq.ssr.ssrfun]
{ mono _ : _ / _ >-> _ } (type_scope) [in Coq.ssr.ssrfun]
{ homo _ : _ _ /~ _ } (type_scope) [in Coq.ssr.ssrfun]
{ homo _ : _ _ / _ } (type_scope) [in Coq.ssr.ssrfun]
{ homo _ : _ _ / _ >-> _ } (type_scope) [in Coq.ssr.ssrfun]
{ homo _ : _ / _ } (type_scope) [in Coq.ssr.ssrfun]
{ homo _ : _ / _ >-> _ } (type_scope) [in Coq.ssr.ssrfun]
{ morph _ : _ _ / _ } (type_scope) [in Coq.ssr.ssrfun]
{ morph _ : _ _ / _ >-> _ } (type_scope) [in Coq.ssr.ssrfun]
{ morph _ : _ / _ } (type_scope) [in Coq.ssr.ssrfun]
{ morph _ : _ / _ >-> _ } (type_scope) [in Coq.ssr.ssrfun]
{ type of _ for _ } (type_scope) [in Coq.ssr.ssreflect]
_ * _ (type_scope) [in Coq.Init.Datatypes]
_ + _ (type_scope) [in Coq.Init.Datatypes]
{ ( _ , _ ) : _ | _ } (type_scope) [in Coq.Program.Utils]
_ ^ _ (type_scope) [in Coq.Numbers.NaryFunctions]
_ ^^ _ --> _ (type_scope) [in Coq.Numbers.NaryFunctions]
() (type_scope) [in Coq.Program.Syntax]
_ ≠ _ (type_scope) [in Coq.Unicode.Utf8_core]
¬ _ (type_scope) [in Coq.Unicode.Utf8_core]
_ ↔ _ (type_scope) [in Coq.Unicode.Utf8_core]
_ → _ (type_scope) [in Coq.Unicode.Utf8_core]
_ ∧ _ (type_scope) [in Coq.Unicode.Utf8_core]
_ ∨ _ (type_scope) [in Coq.Unicode.Utf8_core]
∃ _ .. _ , _ (type_scope) [in Coq.Unicode.Utf8_core]
∀ _ .. _ , _ (type_scope) [in Coq.Unicode.Utf8_core]
_ ^^ _ (Z_scope) [in Coq.ZArith.Zpow_alt]
_ < _ <= _ (Z_scope) [in Coq.ZArith.BinInt]
_ < _ < _ (Z_scope) [in Coq.ZArith.BinInt]
_ <= _ < _ (Z_scope) [in Coq.ZArith.BinInt]
_ <= _ <= _ (Z_scope) [in Coq.ZArith.BinInt]
_ > _ (Z_scope) [in Coq.ZArith.BinInt]
_ >= _ (Z_scope) [in Coq.ZArith.BinInt]
_ < _ (Z_scope) [in Coq.ZArith.BinInt]
_ <= _ (Z_scope) [in Coq.ZArith.BinInt]
( _ | _ ) (Z_scope) [in Coq.ZArith.BinInt]
_ >? _ (Z_scope) [in Coq.ZArith.BinInt]
_ >=? _ (Z_scope) [in Coq.ZArith.BinInt]
_ [in Coq.ZArith.BinInt]
_ <=? _ (Z_scope) [in Coq.ZArith.BinInt]
_ =? _ (Z_scope) [in Coq.ZArith.BinInt]
_ ?= _ (Z_scope) [in Coq.ZArith.BinInt]
_ ÷ _ (Z_scope) [in Coq.ZArith.BinInt]
_ mod _ (Z_scope) [in Coq.ZArith.BinInt]
_ / _ (Z_scope) [in Coq.ZArith.BinInt]
_ ^ _ (Z_scope) [in Coq.ZArith.BinInt]
_ * _ (Z_scope) [in Coq.ZArith.BinInt]
_ - _ (Z_scope) [in Coq.ZArith.BinInt]
- _ (Z_scope) [in Coq.ZArith.BinInt]
_ + _ (Z_scope) [in Coq.ZArith.BinInt]
' _ (Z_scope) [in Coq.QArith.QArith_base]
_ ^ _ [in Coq.Numbers.NatInt.NZDomain]
_ == _ [in Coq.NArith.Ndigits]
_ + _ [in Coq.Structures.OrdersTac]
_ =_D _ [in Coq.Reals.Rtopology]
_ <>b _ [in Coq.Classes.SetoidDec]
_ ==b _ [in Coq.Classes.SetoidDec]
_ =/= _ [in Coq.Classes.SetoidDec]
_ == _ [in Coq.Classes.SetoidDec]
_ ≥ _ [in Coq.Unicode.Utf8]
_ ≤ _ [in Coq.Unicode.Utf8]
_ ^ _ [in Coq.setoid_ring.Algebra_syntax]
_ == _ [in Coq.setoid_ring.Algebra_syntax]
_ - _ [in Coq.setoid_ring.Algebra_syntax]
_ * _ [in Coq.setoid_ring.Algebra_syntax]
_ + _ [in Coq.setoid_ring.Algebra_syntax]
_ (* _ *) [in Coq.ssr.ssreflect]
_ :: _ [in Coq.Classes.RelationClasses]
_ [@ _ ] [in Coq.Vectors.VectorDef]
_ :: _ [in Coq.Vectors.VectorDef]
_ ~= _ [in Coq.Program.Equality]
_ \ _ [in Coq.rtauto.Bintree]
_ <>b _ [in Coq.Classes.EquivDec]
_ ==b _ [in Coq.Classes.EquivDec]
_ \\// _ [in Coq.rtauto.Rtauto]
_ //\\ _ [in Coq.rtauto.Rtauto]
_ =>> _ [in Coq.rtauto.Rtauto]
rew dependent _ in _ [in Coq.Init.Logic]
rew dependent _ in _ [in Coq.Init.Specif]
Set [in Coq.Logic.SetIsType]
_==_ [in Coq.setoid_ring.Algebra_syntax]
_-_ [in Coq.setoid_ring.Algebra_syntax]
_*_ [in Coq.setoid_ring.Algebra_syntax]
_+_ [in Coq.setoid_ring.Algebra_syntax]
# [in Coq.rtauto.Rtauto]
() [in Coq.Program.Syntax]
-_ [in Coq.setoid_ring.Algebra_syntax]
- _ [in Coq.setoid_ring.Algebra_syntax]
0 [in Coq.setoid_ring.Algebra_syntax]
1 [in Coq.setoid_ring.Algebra_syntax]
[in Coq.ssr.ssreflect]
@ sval [in Coq.ssr.ssrfun]
@ comp [in Coq.ssr.ssrfun]
[ _ ; .. ; _ ] [in Coq.Sorting.PermutSetoid]
[ ] [in Coq.Sorting.PermutSetoid]
[ _ ] [in Coq.setoid_ring.Algebra_syntax]
[ _ ; .. ; _ ] [in Coq.Sorting.Mergesort]
[ ] [in Coq.Sorting.Mergesort]
[ ] [in Coq.Vectors.VectorDef]
[ _ ; .. ; _ ] [in Coq.Sorting.Sorted]
[ ] [in Coq.Sorting.Sorted]
[ _ ] [in Coq.rtauto.Rtauto]
{ all3 _ } [in Coq.ssr.ssrbool]
{ all2 _ } [in Coq.ssr.ssrbool]
{ all1 _ } [in Coq.ssr.ssrbool]
λ _ .. _ , _ [in Coq.Unicode.Utf8_core]



Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (21445 entries)
Notation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (889 entries)
Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (714 entries)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1464 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (482 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (10031 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (663 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (537 entries)
Projection Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (374 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (285 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (457 entries)
Instance Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (616 entries)
Abbreviation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1328 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (3468 entries)
Record Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (137 entries)