helm/ocaml/cic_notation/doc/samples.ma

   1
   2 notation
   3   "\langle a , b \rangle"
   4 for
   5   @{ 'pair $a $b }.
   6 check \langle 1, \langle 2, 3 \rangle \rangle.
   7 check 'pair 1 ('pair 2 ('pair 3 4)).
   8
   9 notation "a :: b" for @{ 'cons $a $b }.
  10 check 1 :: 2 :: 'ugo.
  11
  12 notation
  13   "[ hovbox (list0 a sep ; ) ]"
  14 for ${
  15   fold right
  16     @'nil
  17   rec acc
  18     @{ 'cons $a $acc }
  19 }.
  20 check [1;2;3;4].
  21
  22 notation
  23   "[ list1 a sep ; | b ]"
  24 for ${
  25   if @{ 'cons $_ $_ } then
  26     fold right
  27       if @'nil then
  28         fail
  29       else if @{ 'cons $_ $_ } then
  30         fail
  31       else
  32         b
  33     rec acc
  34       @{ 'cons $a $acc }
  35   else
  36     fail
  37 }.
  38 check 'cons 1 ('cons 2 ('cons 3 'ugo)).
  39 check 'cons 1 ('cons 2 ('cons 3 'nil)).
  40 check [1;2;3;4].
  41 check [1;2;3;4|5].
  42
  43 notation "a + b" left associative for @{ 'plus $a $b }.
  44 check 1 + 2 + 3.
  45 check 1 + (2 + 3).
  46
  47 notation "a + b" left associative for @{ 'plus $a $b }.
  48 notation "a * b" left associative for @{ 'mult $a $b }.
  49 interpretation 'plus x y = (cic:/Coq/Init/Peano/plus.con x y).
  50 interpretation 'mult x y = (cic:/Coq/Init/Peano/mult.con x y).
  51 render cic:/Coq/Arith/Mult/mult_plus_distr_r.con.
  52
  53 notation
  54   "hvbox ('if' a 'then' break b break 'else' break c)"
  55 for
  56   @{ 'ifthenelse $a $b $c }.
  57 check if even then \forall x:nat.x else bump x.
  58
  59 notation
  60   "a \vee b"
  61 for
  62   @{ if $a > $b then $a else $b }
  63
  64 notation
  65   "'fun' ident x \to a"
  66   right associative with precedence 20
  67 for
  68   @{ 'lambda ${ident x} $a }.
  69
  70 notation
  71   "hvbox(a break \to b)"
  72 for
  73   @{ \forall $_:$a.$b }.
  74 check nat \to nat.
  75
  76 NOTES
  77
  78 @a e' un'abbreviazione per @{term a}
  79 "x" e' un'abbreviazione per @{keyword x}
  80 @_ e' un'abbreviazione per @{anonymous}
  81
  82 \x simbolo della sintassi concreta
  83 'x simbolo della sintassi astratta
  84
  85 \lbrace \rbrace per le parentesi graffe al livello 1
  86
  87 OLD SAMPLES
  88
  89 # sample mappings level 1 <--> level 2
  90
  91 notation \[ \TERM a ++ \OPT \NUM i \] for 'assign \TERM a ('plus \TERM a \DEFAULT \[\NUM i\] \[1\]).
  92 check 1 ++ 2.
  93
  94 notation \[ + \LIST0 \NUM a \] for \FOLD right \[ 'zero \] \LAMBDA acc \[ 'plus \NUM a \TERM acc \].
  95 check + 1 2 3 4.
  96
  97 notation \[ [ \HOVBOX\[ \LIST0 \TERM a \SEP ; \] ] \] for \FOLD right \[ 'nil \] \LAMBDA acc \[ 'cons \TERM a \TERM acc \].
  98 check [].
  99 check [1;2;3;4].
 100
 101 notation \[ [ \LIST0 \[ \TERM a ; \TERM b \] \SEP ; ] \] for \FOLD right \[ 'nil \] \LAMBDA acc \[ 'cons \TERM a ( 'cons \TERM b \TERM acc) \] .
 102 check [].
 103 check [1;2].
 104 check [1;2;3;4].
 105
 106 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 \] .
 107
 108 notation \[ | \LIST0 \[ \OPT \[ \NUM i \] \] \SEP ; | \] for \FOLD right \[ 'nil \] \LAMBDA acc \[ 'cons \DEFAULT \[ 'Some \NUM i \] \[ 'None \] \TERM acc \] .
 109
 110 # sample mappings level 2 <--> level 3
 111
 112 interpretation 'plus x y = (cic:/Coq/Init/Peano/plus.con x y).
 113 interpretation 'mult x y = (cic:/Coq/Init/Peano/mult.con x y).
 114 render cic:/Coq/Arith/Mult/mult_plus_distr_r.con.
 115
 116 notation \[ \TERM a \OVER \TERM b : \TERM c \SQRT \TERM d \] for 'megacoso \TERM a \TERM b \TERM c \TERM d.
 117 interpretation "megacoso" 'megacoso x y z w =
 118   (cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)
 119     cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)
 120     (cic:/Coq/Init/Peano/plus.con x y)
 121     (cic:/Coq/Init/Peano/plus.con z w)).
 122 render cic:/Coq/Arith/Plus/plus_comm.con.
 123
 124 # full samples
 125
 126 notation \[ \TERM a + \TERM b \] for 'plus \TERM a \TERM b.
 127 check 1 + 2.
 128 interpretation 'plus x y = (cic:/Coq/Init/Peano/plus.con x y).
 129 render cic:/Coq/Arith/Plus/plus_comm.con.
 130
 131 notation \[ \TERM a + \TERM b \] left associative with precedence 50 for 'plus \TERM a \TERM b.
 132 notation \[ \TERM a * \TERM b \] left associative with precedence 60 for 'mult \TERM a \TERM b.
 133 interpretation 'plus x y = (cic:/Coq/Init/Peano/plus.con x y).
 134 interpretation 'mult x y = (cic:/Coq/Init/Peano/mult.con x y).
 135 render cic:/Coq/Arith/Mult/mult_plus_distr_r.con.
 136
 137 notation \[ \LIST \NUM a \] for \FOLD left \[ 'a \] \LAMBDA acc \[ 'b \NUM a \].
 138
 139