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___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
25 (* \VV/ *************************************************************)
27 (* // * This file is distributed under the terms of the *)
29 (* * GNU Lesser General Public License Version 2.1 *)
31 (*#**********************************************************************)
33 (*#* Syntax for arithmetic *)
35 include "Num/Params.ma".
38 Infix 6 "<" lt V8only 70.
42 Infix 6 "<=" le V8only 70.
46 Infix 6 ">" gt V8only 70.
50 Infix 6 ">=" ge V8only 70.
53 (*i Infix 7 "+" plus V8only 50. i*)
56 Grammar constr lassoc_constr4 :=
58 [ lassoc_constr4($c1) "+" lassoc_constr4($c2) ] ->
62 (SQUASH $T1) -> [ (sumbool $T1 $T2) ] (* {T1}+{T2} *)
63 | $_ -> [ (sumor $c1 $T2) ] (* c1+{T2} *)
65 | $_ -> [ (add $c1 $c2) ] (* c1+c2 *)
72 sum [ (add $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "+" $t2:L ] ]