]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_disambiguation/doc/precedence.txt
ocaml 3.09 transition
[helm.git] / helm / ocaml / cic_disambiguation / doc / precedence.txt
index cd7186fcf6a3ace26de12020692f93bf5b024d9a..09efea85377c901b96b2ef142f59c7723dd6842c 100644 (file)
@@ -2,7 +2,7 @@
 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
@@ -10,7 +10,7 @@ S x = y                  (= (S x) y)                   apply  > infix operators
 
 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)
 
@@ -25,7 +25,7 @@ EOT
   
 should respond with:
   
-  (\lambda x.x y)
+  \lambda x.(x y)
   (eq (S x) y)
   \forall x.(eq x x)
   \lambda x.(x \to x)