]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/cic_disambiguation/doc/precedence.txt
tex macros, checked in disambiguation section from whelp paper
[helm.git] / helm / ocaml / 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