Input Should be parsed as Derived constraint
on precedence
--------------------------------------------------------------------------------
-\lambda x.x y ((\lambda x.x) y) lambda > apply
+\lambda x.x y \lambda x.(x y) lambda > apply
S x = y (= (S x) y) apply > infix operators
\forall x.x=x (\forall x.(= x x)) infix operators > binders
\lambda x.x \to x \lambda. (x \to x) \to > \lambda
Precedence total order:
- \to > lambda > apply > infix operators > binders
+ apply > infix operators > to > binders
where binders are all binders except lambda (i.e. \forall, \pi, \exists)
+to test:
+
+./test_parser term << EOT
+ \lambda x.x y
+ S x = y
+ \forall x.x=x
+ \lambda x.x \to x
+EOT
+
+should respond with:
+
+ \lambda x.(x y)
+ (eq (S x) y)
+ \forall x.(eq x x)
+ \lambda x.(x \to x)
+