Reshaped structure of ocaml/ libraries.

[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
deleted file mode 100644 (file)
index ff63801..0000000
--- a/helm/ocaml/cic_notation/doc/samples.ma
+++ /dev/null
@@ -1,139 +0,0 @@
-
-notation
-  "\langle a , b \rangle"
-for
-  @{ 'pair $a $b }.
-check \langle 1, \langle 2, 3 \rangle \rangle.
-check 'pair 1 ('pair 2 ('pair 3 4)).
-
-notation "a :: b" for @{ 'cons $a $b }.
-check 1 :: 2 :: 'ugo.
-
-notation
-  "[ hovbox (list0 a sep ; ) ]"
-for ${
-  fold right
-    @'nil
-  rec acc
-    @{ 'cons $a $acc }
-}.
-check [1;2;3;4].
-
-notation
-  "[ list1 a sep ; | b ]"
-for ${
-  if @{ 'cons $_ $_ } then
-    fold right
-      if @'nil then
-        fail
-      else if @{ 'cons $_ $_ } then
-        fail
-      else
-        b
-    rec acc
-      @{ 'cons $a $acc }
-  else
-    fail
-}.
-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 }.
-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 }.
-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
-  "hvbox ('if' a 'then' break b break 'else' break c)"
-for
-  @{ 'ifthenelse $a $b $c }.
-check if even then \forall x:nat.x else bump x.
-
-notation
-  "a \vee b"
-for
-  @{ if $a > $b then $a else $b }
-
-notation
-  "'fun' ident x \to a"
-  right associative with precedence 20
-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}
-"x" e' un'abbreviazione per @{keyword x}
-@_ e' un'abbreviazione per @{anonymous}
-
-\x simbolo della sintassi concreta
-'x simbolo della sintassi astratta
-
-\lbrace \rbrace per le parentesi graffe al livello 1
-
-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\]).
-check 1 ++ 2.
-
-notation \[ + \LIST0 \NUM a \] for \FOLD right \[ 'zero \] \LAMBDA acc \[ 'plus \NUM a \TERM acc \].
-check + 1 2 3 4.
-
-notation \[ [ \HOVBOX\[ \LIST0 \TERM a \SEP ; \] ] \] for \FOLD right \[ 'nil \] \LAMBDA acc \[ 'cons \TERM a \TERM acc \].
-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) \] .
-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 \] .  
-
-notation \[ | \LIST0 \[ \OPT \[ \NUM i \] \] \SEP ; | \] for \FOLD right \[ 'nil \] \LAMBDA acc \[ 'cons \DEFAULT \[ 'Some \NUM i \] \[ 'None \] \TERM acc \] .
-
-# sample mappings level 2 <--> level 3
-
-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 \[ \TERM a \OVER \TERM b : \TERM c \SQRT \TERM d \] for 'megacoso \TERM a \TERM b \TERM c \TERM d.
-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.
-check 1 + 2.
-interpretation 'plus x y = (cic:/Coq/Init/Peano/plus.con x y).
-render cic:/Coq/Arith/Plus/plus_comm.con.
-
-notation \[ \TERM a + \TERM b \] left associative with precedence 50 for 'plus \TERM a \TERM b.
-notation \[ \TERM a * \TERM b \] left associative with precedence 60 for 'mult \TERM a \TERM 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 \[ \LIST \NUM a \] for \FOLD left \[ 'a \] \LAMBDA acc \[ 'b \NUM a \].
-
-