1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(*i $Id: Notations.v 11073 2008-06-08 20:24:51Z herbelin $ i*)
11
(** These are the notations whose level and associativity are imposed by Coq *)
13
(** Notations for propositional connectives *)
15
Reserved Notation "x <-> y" (at level 95, no associativity).
16
Reserved Notation "x /\ y" (at level 80, right associativity).
17
Reserved Notation "x \/ y" (at level 85, right associativity).
18
Reserved Notation "~ x" (at level 75, right associativity).
20
(** Notations for equality and inequalities *)
22
Reserved Notation "x = y :> T"
23
(at level 70, y at next level, no associativity).
24
Reserved Notation "x = y" (at level 70, no associativity).
25
Reserved Notation "x = y = z"
26
(at level 70, no associativity, y at next level).
28
Reserved Notation "x <> y :> T"
29
(at level 70, y at next level, no associativity).
30
Reserved Notation "x <> y" (at level 70, no associativity).
32
Reserved Notation "x <= y" (at level 70, no associativity).
33
Reserved Notation "x < y" (at level 70, no associativity).
34
Reserved Notation "x >= y" (at level 70, no associativity).
35
Reserved Notation "x > y" (at level 70, no associativity).
37
Reserved Notation "x <= y <= z" (at level 70, y at next level).
38
Reserved Notation "x <= y < z" (at level 70, y at next level).
39
Reserved Notation "x < y < z" (at level 70, y at next level).
40
Reserved Notation "x < y <= z" (at level 70, y at next level).
42
(** Arithmetical notations (also used for type constructors) *)
44
Reserved Notation "x + y" (at level 50, left associativity).
45
Reserved Notation "x - y" (at level 50, left associativity).
46
Reserved Notation "x * y" (at level 40, left associativity).
47
Reserved Notation "x / y" (at level 40, left associativity).
48
Reserved Notation "- x" (at level 35, right associativity).
49
Reserved Notation "/ x" (at level 35, right associativity).
50
Reserved Notation "x ^ y" (at level 30, right associativity).
52
(** Notations for booleans *)
54
Reserved Notation "x || y" (at level 50, left associativity).
55
Reserved Notation "x && y" (at level 40, left associativity).
57
(** Notations for pairs *)
59
Reserved Notation "( x , y , .. , z )" (at level 0).
61
(** Notation "{ x }" is reserved and has a special status as component
62
of other notations such as "{ A } + { B }" and "A + { B }" (which
63
are at the same level than "x + y");
64
"{ x }" is at level 0 to factor with "{ x : A | P }" *)
66
Reserved Notation "{ x }" (at level 0, x at level 99).
68
(** Notations for sigma-types or subsets *)
70
Reserved Notation "{ x | P }" (at level 0, x at level 99).
71
Reserved Notation "{ x | P & Q }" (at level 0, x at level 99).
73
Reserved Notation "{ x : A | P }" (at level 0, x at level 99).
74
Reserved Notation "{ x : A | P & Q }" (at level 0, x at level 99).
76
Reserved Notation "{ x : A & P }" (at level 0, x at level 99).
77
Reserved Notation "{ x : A & P & Q }" (at level 0, x at level 99).
79
Delimit Scope type_scope with type.
80
Delimit Scope core_scope with core.
82
Open Scope core_scope.
83
Open Scope type_scope.