fixed precedence of \to

[helm.git] / helm / ocaml / cic_disambiguation / doc / precedence.txt

diff --git a/helm/ocaml/cic_disambiguation/doc/precedence.txt b/helm/ocaml/cic_disambiguation/doc/precedence.txt
index f0a91418d3f64c24a3861a23a14eaa5e68a071d9..cd7186fcf6a3ace26de12020692f93bf5b024d9a 100644 (file)
--- a/helm/ocaml/cic_disambiguation/doc/precedence.txt
+++ b/helm/ocaml/cic_disambiguation/doc/precedence.txt
@@ -14,3 +14,19 @@ Precedence total order:
 
 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)
+