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 | (72679 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 | (1040 entries) |

Binder 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 | (47172 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 | (791 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 | (1553 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 | (585 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 | (11862 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 | (1030 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 | (625 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 | (308 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 | (474 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 | (493 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 | (896 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 | (1443 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 | (4242 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 | (165 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 an _ (bool_scope) [notation, in Coq.ssr.ssrbool]

_ \is a _ (bool_scope) [notation, in Coq.ssr.ssrbool]

_ \is a _ (bool_scope) [notation, in Coq.ssr.ssrbool]

_ \is _ (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]

_ <? _ (char_scope) [notation, in Coq.Strings.Ascii]

_ ?= _ (char_scope) [notation, in Coq.Strings.Ascii]

_ =? _ (char_scope) [notation, in Coq.Strings.Ascii]

_ * _ (ConstructiveReals) [notation, in Coq.Reals.Abstract.ConstructiveReals]

_ - _ (ConstructiveReals) [notation, in Coq.Reals.Abstract.ConstructiveReals]

_ + _ (ConstructiveReals) [notation, in Coq.Reals.Abstract.ConstructiveReals]

_ ≶ _ (ConstructiveReals) [notation, in Coq.Reals.Abstract.ConstructiveReals]

_ == _ (ConstructiveReals) [notation, in Coq.Reals.Abstract.ConstructiveReals]

_ < _ < _ (ConstructiveReals) [notation, in Coq.Reals.Abstract.ConstructiveReals]

_ <= _ <= _ (ConstructiveReals) [notation, in Coq.Reals.Abstract.ConstructiveReals]

_ <= _ (ConstructiveReals) [notation, in Coq.Reals.Abstract.ConstructiveReals]

_ < _ (ConstructiveReals) [notation, in Coq.Reals.Abstract.ConstructiveReals]

- _ (ConstructiveReals) [notation, in Coq.Reals.Abstract.ConstructiveReals]

/ _ (ConstructiveReals) [notation, in Coq.Reals.Abstract.ConstructiveReals]

0 (ConstructiveReals) [notation, in Coq.Reals.Abstract.ConstructiveReals]

1 (ConstructiveReals) [notation, in Coq.Reals.Abstract.ConstructiveReals]

10 (ConstructiveReals) [notation, in Coq.Reals.Abstract.ConstructiveReals]

2 (ConstructiveReals) [notation, in Coq.Reals.Abstract.ConstructiveReals]

3 (ConstructiveReals) [notation, in Coq.Reals.Abstract.ConstructiveReals]

4 (ConstructiveReals) [notation, in Coq.Reals.Abstract.ConstructiveReals]

5 (ConstructiveReals) [notation, in Coq.Reals.Abstract.ConstructiveReals]

6 (ConstructiveReals) [notation, in Coq.Reals.Abstract.ConstructiveReals]

7 (ConstructiveReals) [notation, in Coq.Reals.Abstract.ConstructiveReals]

8 (ConstructiveReals) [notation, in Coq.Reals.Abstract.ConstructiveReals]

9 (ConstructiveReals) [notation, in Coq.Reals.Abstract.ConstructiveReals]

_ : 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]

_ - _ (CReal_scope) [notation, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

- _ (CReal_scope) [notation, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

_ + _ (CReal_scope) [notation, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

2 (CReal_scope) [notation, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

1 (CReal_scope) [notation, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

0 (CReal_scope) [notation, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

_ == _ (CReal_scope) [notation, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

_ < _ <= _ (CReal_scope) [notation, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

_ < _ < _ (CReal_scope) [notation, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

_ <= _ < _ (CReal_scope) [notation, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

_ <= _ <= _ (CReal_scope) [notation, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

_ >= _ (CReal_scope) [notation, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

_ <= _ (CReal_scope) [notation, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

_ # _ (CReal_scope) [notation, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

_ > _ (CReal_scope) [notation, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

_ < _ (CReal_scope) [notation, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

/ _ (CReal_scope) [notation, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]

_ * _ (CReal_scope) [notation, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]

_ =~= _ (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]

_ *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]

_ +++ _ (list_scope) [notation, in Coq.micromega.Refl]

( _ | _ ) (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]

_ <? _ (nat_scope) [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]

_ 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]

_ <? _ (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.Nat]

_ mod _ (nat_scope) [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]

_ <=? _ (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]

_ <? _ (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]

_ + _ (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]

( _ | _ ) (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]

_ <? _ (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]

_ ~ 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]

_ ^ _ (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]

_ < _ (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]

_ ^Z _ (R_scope) [notation, in Coq.Reals.Rfunctions]

_ ^ _ (R_scope) [notation, in Coq.Reals.Rfunctions]

_ / _ (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]

_ ² (R_scope) [notation, in Coq.Reals.RIneq]

_ * _ (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]

<hidden _ > (ssr_scope) [notation, in Coq.ssr.ssreflect]

_ ++ _ (string_scope) [notation, in Coq.Strings.String]

_ <=? _ (string_scope) [notation, in Coq.Strings.String]

_ <? _ (string_scope) [notation, in Coq.Strings.String]

_ ?= _ (string_scope) [notation, in Coq.Strings.String]

_ =? _ (string_scope) [notation, in Coq.Strings.String]

_ ^ _ (type_scope) [notation, in Coq.Numbers.NaryFunctions]

_ ^^ _ --> _ (type_scope) [notation, in Coq.Numbers.NaryFunctions]

_ + { _ } (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]

{ _ : _ | _ } (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]

{ 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.Classes.SetoidClass]

_ =/= _ (type_scope) [notation, in Coq.Classes.SetoidClass]

_ == _ (type_scope) [notation, in Coq.Classes.SetoidClass]

_ * _ (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.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]

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]

_ <-> _ (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.Program.Utils]

_ *c _ (uint63_scope) [notation, in Coq.Numbers.Cyclic.Int63.Cyclic63]

_ ≡ _ (uint63_scope) [notation, in Coq.Numbers.Cyclic.Int63.Uint63]

[-| _ |] (uint63_scope) [notation, in Coq.Numbers.Cyclic.Int63.Uint63]

[+| _ |] (uint63_scope) [notation, in Coq.Numbers.Cyclic.Int63.Uint63]

_ < _ <= _ (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]

_ <? _ (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]

_ 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.ZArith.Zpow_alt]

_ || _ [notation, in Coq.Strings.HexString]

_ :: _ [notation, in Coq.Classes.RelationClasses]

_ .3 [notation, in Coq.Init.Specif]

_ ^ _ [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.Program.Equality]

_ \ _ [notation, in Coq.rtauto.Bintree]

_ <>b _ [notation, in Coq.Classes.EquivDec]

_ ==b _ [notation, in Coq.Classes.EquivDec]

_ ^ _ [notation, in Coq.Numbers.NatInt.NZDomain]

_ == _ [notation, in Coq.NArith.Ndigits]

_ =_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.Structures.OrdersTac]

_ ≥ _ [notation, in Coq.Unicode.Utf8]

_ ≤ _ [notation, in Coq.Unicode.Utf8]

_ [@ _ ] [notation, in Coq.Vectors.VectorDef]

_ :: _ [notation, in Coq.Vectors.VectorDef]

_ \\// _ [notation, in Coq.rtauto.Rtauto]

_ //\\ _ [notation, in Coq.rtauto.Rtauto]

_ =>> _ [notation, in Coq.rtauto.Rtauto]

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.Program.Syntax]

-_ [notation, in Coq.setoid_ring.Algebra_syntax]

- _ [notation, in Coq.setoid_ring.Algebra_syntax]

0 [notation, in Coq.Init.Byte]

0 [notation, in Coq.ZArith.BinIntDef]

0 [notation, in Coq.Init.Peano]

0 [notation, in Coq.Init.Nat]

0 [notation, in Coq.setoid_ring.Algebra_syntax]

0 [notation, in Coq.NArith.BinNatDef]

1 [notation, in Coq.Init.Byte]

1 [notation, in Coq.ZArith.BinIntDef]

1 [notation, in Coq.Init.Nat]

1 [notation, in Coq.setoid_ring.Algebra_syntax]

1 [notation, in Coq.NArith.BinNatDef]

1 [notation, in Coq.PArith.BinPosDef]

2 [notation, in Coq.ZArith.BinIntDef]

2 [notation, in Coq.Init.Nat]

2 [notation, in Coq.NArith.BinNatDef]

@ 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.Sorted]

[ ] [notation, in Coq.Sorting.Sorted]

[ _ ; .. ; _ ] [notation, in Coq.Sorting.Mergesort]

[ ] [notation, in Coq.Sorting.Mergesort]

[ ] [notation, in Coq.Vectors.VectorDef]

[ _ ] [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 | 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 | (72679 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 | (1040 entries) |

Binder 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 | (47172 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 | (791 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 | (1553 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 | (585 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 | (11862 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 | (1030 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 | (625 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 | (308 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 | (474 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 | (493 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 | (896 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 | (1443 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 | (4242 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 | (165 entries) |