]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/doc/samples.ma
snapshot
[helm.git] / helm / ocaml / cic_notation / doc / samples.ma
index f1f6ac9391178a8b171c5d9fd1b8b682e086a813..46193bf73d90aea14c1493fb1e85fa7f998799a9 100644 (file)
@@ -51,8 +51,7 @@ notation
   "'if' a 'then' b 'else' c"
 for
   @{ 'ifthenelse $a $b $c }.
-
-TODO collezionare le keyword e aggiungerle al lexer nonche' ricordarsele per quando si rimuove la notazione.
+print if even then x else bump x.
 
 notation
   "a \vee b"
@@ -61,9 +60,9 @@ for
 
 notation
   "'fun' ident x \to a"
-  right associative at precedence ...
+  right associative with precedence 20
 for
-  @{ 'lambda ${ident x} $a }
+  @{ 'lambda ${ident x} $a }.
 
 NOTES