ocaml 3.09 transition

[helm.git] / helm / ocaml / cic_notation / doc / samples.ma

diff --git a/helm/ocaml/cic_notation/doc/samples.ma b/helm/ocaml/cic_notation/doc/samples.ma
index 493db5958912e08f2a41dc78e591cb9fe379fe48..ff6380151876bf82ecc32778e96afccd30e57f2a 100644 (file)
--- a/helm/ocaml/cic_notation/doc/samples.ma
+++ b/helm/ocaml/cic_notation/doc/samples.ma
@@ -3,14 +3,11 @@ notation
   "\langle a , b \rangle"
 for
   @{ 'pair $a $b }.
-print \langle 1, \langle 2, 3 \rangle \rangle.
-print 'pair 1 ('pair 2 ('pair 3 4)).
+check \langle 1, \langle 2, 3 \rangle \rangle.
+check 'pair 1 ('pair 2 ('pair 3 4)).
 
-notation
-  "a :: b"
-for
-  @{ 'cons $a $b }.
-print 1 :: 2 :: 'ugo.
+notation "a :: b" for @{ 'cons $a $b }.
+check 1 :: 2 :: 'ugo.
 
 notation
   "[ hovbox (list0 a sep ; ) ]"
@@ -20,7 +17,7 @@ for ${
   rec acc
     @{ 'cons $a $acc }
 }.
-print [1;2;3;4].
+check [1;2;3;4].
 
 notation
   "[ list1 a sep ; | b ]"
@@ -38,14 +35,14 @@ for ${
   else
     fail
 }.
-print 'cons 1 ('cons 2 ('cons 3 'ugo)).
-print 'cons 1 ('cons 2 ('cons 3 'nil)).
-print [1;2;3;4].
-print [1;2;3;4|5].
+check 'cons 1 ('cons 2 ('cons 3 'ugo)).
+check 'cons 1 ('cons 2 ('cons 3 'nil)).
+check [1;2;3;4].
+check [1;2;3;4|5].
 
 notation "a + b" left associative for @{ 'plus $a $b }.
-print 1 + 2 + 3.
-print 1 + (2 + 3).
+check 1 + 2 + 3.
+check 1 + (2 + 3).
 
 notation "a + b" left associative for @{ 'plus $a $b }.
 notation "a * b" left associative for @{ 'mult $a $b }.
@@ -57,7 +54,7 @@ notation
   "hvbox ('if' a 'then' break b break 'else' break c)"
 for
   @{ 'ifthenelse $a $b $c }.
-print if even then \forall x:nat.x else bump x.
+check if even then \forall x:nat.x else bump x.
 
 notation
   "a \vee b"
@@ -70,6 +67,12 @@ notation
 for
   @{ 'lambda ${ident x} $a }.
 
+notation
+  "hvbox(a break \to b)"
+for
+  @{ \forall $_:$a.$b }.
+check nat \to nat.
+
 NOTES
 
 @a e' un'abbreviazione per @{term a}
@@ -86,19 +89,19 @@ OLD SAMPLES
 # sample mappings level 1 <--> level 2
 
 notation \[ \TERM a ++ \OPT \NUM i \] for 'assign \TERM a ('plus \TERM a \DEFAULT \[\NUM i\] \[1\]).
-print 1 ++ 2.
+check 1 ++ 2.
 
 notation \[ + \LIST0 \NUM a \] for \FOLD right \[ 'zero \] \LAMBDA acc \[ 'plus \NUM a \TERM acc \].
-print + 1 2 3 4.
+check + 1 2 3 4.
 
 notation \[ [ \HOVBOX\[ \LIST0 \TERM a \SEP ; \] ] \] for \FOLD right \[ 'nil \] \LAMBDA acc \[ 'cons \TERM a \TERM acc \].
-print [].
-print [1;2;3;4].
+check [].
+check [1;2;3;4].
 
 notation \[ [ \LIST0 \[ \TERM a ; \TERM b \] \SEP ; ] \] for \FOLD right \[ 'nil \] \LAMBDA acc \[ 'cons \TERM a ( 'cons \TERM b \TERM acc) \] .
-print [].
-print [1;2].
-print [1;2;3;4].
+check [].
+check [1;2].
+check [1;2;3;4].
 
 notation \[ | \LIST0 \[ \TERM a \OPT \[ , \TERM b \] \] \SEP ; | \] for \FOLD right \[ 'nil \] \LAMBDA acc \[ 'cons \DEFAULT \[ \TERM a \] \[ ('pair \TERM a \TERM b) \] \TERM acc \] .  
 
@@ -111,13 +114,17 @@ interpretation 'mult x y = (cic:/Coq/Init/Peano/mult.con x y).
 render cic:/Coq/Arith/Mult/mult_plus_distr_r.con.
 
 notation \[ \TERM a \OVER \TERM b : \TERM c \SQRT \TERM d \] for 'megacoso \TERM a \TERM b \TERM c \TERM d.
-interpretation 'megacoso x y z w = (cic:/Coq/Init/Logic/eq.ind#xpointer(1/1) cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1) (cic:/Coq/Init/Peano/plus.con x y) (cic:/Coq/Init/Peano/plus.con z w)).
+interpretation "megacoso" 'megacoso x y z w =
+  (cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)
+    cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)
+    (cic:/Coq/Init/Peano/plus.con x y)
+    (cic:/Coq/Init/Peano/plus.con z w)).
 render cic:/Coq/Arith/Plus/plus_comm.con.
 
 # full samples
 
 notation \[ \TERM a + \TERM b \] for 'plus \TERM a \TERM b.
-print 1 + 2.
+check 1 + 2.
 interpretation 'plus x y = (cic:/Coq/Init/Peano/plus.con x y).
 render cic:/Coq/Arith/Plus/plus_comm.con.
 
@@ -129,3 +136,4 @@ render cic:/Coq/Arith/Mult/mult_plus_distr_r.con.
 
 notation \[ \LIST \NUM a \] for \FOLD left \[ 'a \] \LAMBDA acc \[ 'b \NUM a \].
 
+