(hopefully) final decision on precedence levels:

[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
new file mode 100644 (file)
index 0000000..82e8d4a
--- /dev/null
+++ b/helm/ocaml/cic_disambiguation/doc/precedence.txt
@@ -0,0 +1,12 @@
+
+Input                  Should be parsed as             Derived constraint
+                                                       on precedence
+--------------------------------------------------------------------------------
+\lambda x.x y          ((\lambda x.x) y)               binder > apply
+S x = y                  (= (S x) y)                   apply  > infix operators
+--------------------------------------------------------------------------------
+
+Precedence total order:
+
+  binder > apply > infix operators
+