# Library Coq.Init.Notations

``` ```
These are the notations whose level and associativity are imposed by Coq
``` ```
Notations for propositional connectives
``` Reserved Notation "x <-> y" (at level 95, no associativity). Reserved Notation "x /\ y" (at level 80, right associativity). Reserved Notation "x \/ y" (at level 85, right associativity). Reserved Notation "~ x" (at level 75, right associativity). ```
Notations for equality and inequalities
``` Reserved Notation "x = y :> T" (at level 70, y at next level, no associativity). Reserved Notation "x = y" (at level 70, no associativity). Reserved Notation "x = y = z" (at level 70, no associativity, y at next level). Reserved Notation "x <> y :> T" (at level 70, y at next level, no associativity). Reserved Notation "x <> y" (at level 70, no associativity). Reserved Notation "x <= y" (at level 70, no associativity). Reserved Notation "x < y" (at level 70, no associativity). Reserved Notation "x >= y" (at level 70, no associativity). Reserved Notation "x > y" (at level 70, no associativity). Reserved Notation "x <= y <= z" (at level 70, y at next level). Reserved Notation "x <= y < z" (at level 70, y at next level). Reserved Notation "x < y < z" (at level 70, y at next level). Reserved Notation "x < y <= z" (at level 70, y at next level). ```
Arithmetical notations (also used for type constructors)
``` Reserved Notation "x + y" (at level 50, left associativity). Reserved Notation "x - y" (at level 50, left associativity). Reserved Notation "x * y" (at level 40, left associativity). Reserved Notation "x / y" (at level 40, left associativity). Reserved Notation "- x" (at level 35, right associativity). Reserved Notation "/ x" (at level 35, right associativity). Reserved Notation "x ^ y" (at level 30, right associativity). ```
Notations for pairs
``` Reserved Notation "( x , y , .. , z )" (at level 0). ```
Notation "{ x }" is reserved and has a special status as component of other notations such as "{ A } + { B }" and "A + { B }" (which are at the same level than "x + y"); "{ x }" is at level 0 to factor with "{ x : A | P }"
``` Reserved Notation "{ x }" (at level 0, x at level 99). ```
Notations for sigma-types or subsets
``` Reserved Notation "{ x | P }" (at level 0, x at level 99). Reserved Notation "{ x | P & Q }" (at level 0, x at level 99). Reserved Notation "{ x : A | P }" (at level 0, x at level 99). Reserved Notation "{ x : A | P & Q }" (at level 0, x at level 99). Reserved Notation "{ x : A & P }" (at level 0, x at level 99). Reserved Notation "{ x : A & P & Q }" (at level 0, x at level 99). Delimit Scope type_scope with type. Delimit Scope core_scope with core. Open Scope core_scope. Open Scope type_scope. ```