helm/software/components/cic_disambiguation/doc/precedence.txt

   1
   2 Input                  Should be parsed as             Derived constraint
   3                                                        on precedence
   4 --------------------------------------------------------------------------------
   5 \lambda x.x y          \lambda x.(x y)               lambda > apply
   6 S x = y                  (= (S x) y)                   apply  > infix operators
   7 \forall x.x=x          (\forall x.(= x x))             infix operators > binders
   8 \lambda x.x \to x    \lambda. (x \to x)                \to > \lambda
   9 --------------------------------------------------------------------------------
  10
  11 Precedence total order:
  12
  13   apply > infix operators > to > binders
  14
  15 where binders are all binders except lambda (i.e. \forall, \pi, \exists)
  16
  17 to test:
  18
  19 ./test_parser term << EOT
  20   \lambda x.x y
  21   S x = y
  22   \forall x.x=x
  23   \lambda x.x \to x
  24 EOT
  25
  26 should respond with:
  27
  28   \lambda x.(x y)
  29   (eq (S x) y)
  30   \forall x.(eq x x)
  31   \lambda x.(x \to x)
  32