X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=components%2Fcic_disambiguation%2Fdoc%2Fprecedence.txt;fp=components%2Fcic_disambiguation%2Fdoc%2Fprecedence.txt;h=09efea85377c901b96b2ef142f59c7723dd6842c;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1

diff --git a/components/cic_disambiguation/doc/precedence.txt b/components/cic_disambiguation/doc/precedence.txt
new file mode 100644
index 000000000..09efea853
--- /dev/null
+++ b/components/cic_disambiguation/doc/precedence.txt
@@ -0,0 +1,32 @@
+
+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:
+
+  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)
+