Input Should be parsed as Derived constraint on precedence -------------------------------------------------------------------------------- \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 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)