1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
19 (*#***********************************************************************)
21 (* v * The Coq Proof Assistant / The Coq Development Team *)
23 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
25 (* \VV/ **************************************************************)
27 (* // * This file is distributed under the terms of the *)
29 (* * GNU Lesser General Public License Version 2.1 *)
31 (*#***********************************************************************)
33 (*i $Id: Notations.v,v 1.24.2.2 2004/08/01 09:36:44 herbelin Exp $ i*)
35 (*#* These are the notations whose level and associativity are imposed by Coq *)
37 (*#* Notations for propositional connectives *)
40 Reserved Notation "x <-> y" (at level 95, no associativity).
44 Reserved Notation "x /\ y" (at level 80, right associativity).
48 Reserved Notation "x \/ y" (at level 85, right associativity).
52 Reserved Notation "~ x" (at level 75, right associativity).
55 (*#* Notations for equality and inequalities *)
58 Reserved Notation "x = y :> T"
59 (at level 70, y at next level, no associativity).
63 Reserved Notation "x = y" (at level 70, no associativity).
67 Reserved Notation "x = y = z"
68 (at level 70, no associativity, y at next level).
72 Reserved Notation "x <> y :> T"
73 (at level 70, y at next level, no associativity).
77 Reserved Notation "x <> y" (at level 70, no associativity).
81 Reserved Notation "x <= y" (at level 70, no associativity).
85 Reserved Notation "x < y" (at level 70, no associativity).
89 Reserved Notation "x >= y" (at level 70, no associativity).
93 Reserved Notation "x > y" (at level 70, no associativity).
97 Reserved Notation "x <= y <= z" (at level 70, y at next level).
101 Reserved Notation "x <= y < z" (at level 70, y at next level).
105 Reserved Notation "x < y < z" (at level 70, y at next level).
109 Reserved Notation "x < y <= z" (at level 70, y at next level).
112 (*#* Arithmetical notations (also used for type constructors) *)
115 Reserved Notation "x + y" (at level 50, left associativity).
119 Reserved Notation "x - y" (at level 50, left associativity).
123 Reserved Notation "x * y" (at level 40, left associativity).
127 Reserved Notation "x / y" (at level 40, left associativity).
131 Reserved Notation "- x" (at level 35, right associativity).
135 Reserved Notation "/ x" (at level 35, right associativity).
139 Reserved Notation "x ^ y" (at level 30, right associativity).
142 (*#* Notations for pairs *)
145 Reserved Notation "( x , y , .. , z )" (at level 0).
148 (*#* Notation "{ x }" is reserved and has a special status as component
149 of other notations; it is at level 0 to factor with {x:A|P} etc *)
152 Reserved Notation "{ x }" (at level 0, x at level 99).
155 (*#* Notations for sum-types *)
158 Reserved Notation "{ A } + { B }" (at level 50, left associativity).
162 Reserved Notation "A + { B }" (at level 50, left associativity).
165 (*#* Notations for sigma-types or subsets *)
168 Reserved Notation "{ x : A | P }" (at level 0, x at level 99).
172 Reserved Notation "{ x : A | P & Q }" (at level 0, x at level 99).
176 Reserved Notation "{ x : A & P }" (at level 0, x at level 99).
180 Reserved Notation "{ x : A & P & Q }" (at level 0, x at level 99).
184 Delimit Scope type_scope with type.
188 Delimit Scope core_scope with core.
192 Open Scope core_scope.
196 Open Scope type_scope.