include "Coq.ma".
-(*s Syntax for arithmetic *)
-
include "Num/Params.ma".
-(* NOTATION
-Infix 6 "<" lt.
-*)
-
-(* NOTATION
-Infix 6 "<=" le.
-*)
-
-(* NOTATION
-Infix 6 ">" gt.
-*)
-
-(* NOTATION
-Infix 6 ">=" ge.
-*)
-
-(*i Infix 7 "+" plus. i*)
-
-(* NOTATION
-Grammar constr lassoc_constr4 :=
- squash_sum
- [ lassoc_constr4($c1) "+" lassoc_constr4($c2) ] ->
- case [$c2] of
- (SQUASH $T2) ->
- case [$c1] of
- (SQUASH $T1) -> [ (sumbool $T1 $T2) ] (* {T1}+{T2} *)
- | $_ -> [ (sumor $c1 $T2) ] (* c1+{T2} *)
- esac
- | $_ -> [ (add $c1 $c2) ] (* c1+c2 *)
- esac.
-*)
-
-(* NOTATION
-Syntax constr
- level 1:
- equal [ (eqN $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "=" $t2:E ] ]
- ;
-
- level 4:
- sum [ (add $t1 $t2) ] -> [ [<hov 0> $t1:E [0 1] "+" $t2:L ] ]
-.
-*)
-