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 (*s Syntax for arithmetic *)
37 (*i Infix 7 "+" plus. i*)
40 Grammar constr lassoc_constr4 :=
42 [ lassoc_constr4($c1) "+" lassoc_constr4($c2) ] ->
46 (SQUASH $T1) -> [ (sumbool $T1 $T2) ] (* {T1}+{T2} *)
47 | $_ -> [ (sumor $c1 $T2) ] (* c1+{T2} *)
49 | $_ -> [ (add $c1 $c2) ] (* c1+c2 *)
56 sum [ (add $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "+" $t2:L ] ]