helm/ocaml/cic_notation/doc/samples.ma

   1 # sample mappings level 1 <--> level 2
   2
   3 notation \[ \TERM a ++ \OPT \NUM i \] for 'assign \TERM a ('plus \TERM a \DEFAULT \[\NUM i\] \[1\]).
   4 print 1 ++ 2.
   5
   6 notation \[ + \LIST0 \NUM a \] for \FOLD right \[ 'zero \] \LAMBDA acc \[ 'plus \NUM a \TERM acc \].
   7 print + 1 2 3 4.
   8
   9 notation \[ [ \LIST0 \TERM a \SEP ; ] \] for \FOLD right \[ 'nil \] \LAMBDA acc \[ 'cons \TERM a \TERM acc \].
  10 print [].
  11 print [1;2;3;4].
  12
  13 notation \[ [ \LIST0 \[ \TERM a ; \TERM b \] \SEP ; ] \] for \FOLD right \[ 'nil \] \LAMBDA acc \[ 'cons \TERM a ( 'cons \TERM b \TERM acc) \] .
  14 print [].
  15 print [1;2].
  16 print [1;2;3;4].
  17
  18 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 \] .
  19
  20 notation \[ | \LIST0 \[ \OPT \[ \NUM i \] \] \SEP ; | \] for \FOLD right \[ 'nil \] \LAMBDA acc \[ 'cons \DEFAULT \[ 'Some \NUM i \] \[ 'None \] \TERM acc \] .
  21
  22 # sample mappings level 2 <--> level 3
  23
  24 interpretation 'plus x y = (cic:/Coq/Init/Peano/plus.con x y).
  25 interpretation 'mult x y = (cic:/Coq/Init/Peano/mult.con x y).
  26 render cic:/Coq/Arith/Mult/mult_plus_distr_r.con.
  27
  28 notation \[ \TERM a \OVER \TERM b : \TERM c \SQRT \TERM d \] for 'megacoso \TERM a \TERM b \TERM c \TERM d.
  29 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)).
  30 render cic:/Coq/Arith/Plus/plus_comm.con.
  31
  32 # full samples
  33
  34 notation \[ \TERM a + \TERM b \] for 'plus \TERM a \TERM b.
  35 print 1 + 2.
  36 interpretation 'plus x y = (cic:/Coq/Init/Peano/plus.con x y).
  37 render cic:/Coq/Arith/Plus/plus_comm.con.
  38
  39 notation \[ \TERM a + \TERM b \] left associative with precedence 50 for 'plus \TERM a \TERM b.
  40 notation \[ \TERM a * \TERM b \] left associative with precedence 60 for 'mult \TERM a \TERM b.
  41 interpretation 'plus x y = (cic:/Coq/Init/Peano/plus.con x y).
  42 interpretation 'mult x y = (cic:/Coq/Init/Peano/mult.con x y).
  43 render cic:/Coq/Arith/Mult/mult_plus_distr_r.con.
  44
  45 notation \[ \LIST \NUM a \] for \FOLD left \[ 'a \] \LAMBDA acc \[ 'b \NUM a \].
  46