]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_disambiguation/doc/precedence.txt
- renamed ocaml/ to components/
[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
deleted file mode 100644 (file)
index 09efea8..0000000
+++ /dev/null
@@ -1,32 +0,0 @@
-
-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)
-