added XmlAttrs attribute for specification of xml attributes directly

[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 46193bf73d90aea14c1493fb1e85fa7f998799a9..f8620ececd5867585f3ba022126a33fabdb58cd2 100644 (file)
--- a/helm/ocaml/cic_notation/doc/samples.ma
+++ b/helm/ocaml/cic_notation/doc/samples.ma
@@ -47,11 +47,17 @@ notation "a + b" left associative for @{ 'plus $a $b }.
 print 1 + 2 + 3.
 print 1 + (2 + 3).
 
+notation "a + b" left associative for @{ 'plus $a $b }.
+notation "a * b" left associative for @{ 'mult $a $b }.
+interpretation 'plus x y = (cic:/Coq/Init/Peano/plus.con x y).
+interpretation 'mult x y = (cic:/Coq/Init/Peano/mult.con x y).
+render cic:/Coq/Arith/Mult/mult_plus_distr_r.con.
+
 notation
   "'if' a 'then' b 'else' c"
 for
   @{ 'ifthenelse $a $b $c }.
-print if even then x else bump x.
+print if even then \forall x:nat.x else bump x.
 
 notation
   "a \vee b"