3 "\langle a , b \rangle"
6 print \langle 1, \langle 2, 3 \rangle \rangle.
7 print 'pair 1 ('pair 2 ('pair 3 4)).
16 "[ hovbox (list0 a sep ; ) ]"
26 "[ list1 a sep ; | b ]"
28 if @{ 'cons $_ $_ } then
32 else if @{ 'cons $_ $_ } then
41 print 'cons 1 ('cons 2 ('cons 3 'ugo)).
42 print 'cons 1 ('cons 2 ('cons 3 'nil)).
46 notation "a + b" left associative for @{ 'plus $a $b }.
50 notation "a + b" left associative for @{ 'plus $a $b }.
51 notation "a * b" left associative for @{ 'mult $a $b }.
52 interpretation 'plus x y = (cic:/Coq/Init/Peano/plus.con x y).
53 interpretation 'mult x y = (cic:/Coq/Init/Peano/mult.con x y).
54 render cic:/Coq/Arith/Mult/mult_plus_distr_r.con.
57 "'if' a 'then' b 'else' c"
59 @{ 'ifthenelse $a $b $c }.
60 print if even then \forall x:nat.x else bump x.
65 @{ if $a > $b then $a else $b }
69 right associative with precedence 20
71 @{ 'lambda ${ident x} $a }.
75 @a e' un'abbreviazione per @{term a}
76 "x" e' un'abbreviazione per @{keyword x}
77 @_ e' un'abbreviazione per @{anonymous}
79 \x simbolo della sintassi concreta
80 'x simbolo della sintassi astratta
82 \lbrace \rbrace per le parentesi graffe al livello 1
86 # sample mappings level 1 <--> level 2
88 notation \[ \TERM a ++ \OPT \NUM i \] for 'assign \TERM a ('plus \TERM a \DEFAULT \[\NUM i\] \[1\]).
91 notation \[ + \LIST0 \NUM a \] for \FOLD right \[ 'zero \] \LAMBDA acc \[ 'plus \NUM a \TERM acc \].
94 notation \[ [ \HOVBOX\[ \LIST0 \TERM a \SEP ; \] ] \] for \FOLD right \[ 'nil \] \LAMBDA acc \[ 'cons \TERM a \TERM acc \].
98 notation \[ [ \LIST0 \[ \TERM a ; \TERM b \] \SEP ; ] \] for \FOLD right \[ 'nil \] \LAMBDA acc \[ 'cons \TERM a ( 'cons \TERM b \TERM acc) \] .
103 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 \] .
105 notation \[ | \LIST0 \[ \OPT \[ \NUM i \] \] \SEP ; | \] for \FOLD right \[ 'nil \] \LAMBDA acc \[ 'cons \DEFAULT \[ 'Some \NUM i \] \[ 'None \] \TERM acc \] .
107 # sample mappings level 2 <--> level 3
109 interpretation 'plus x y = (cic:/Coq/Init/Peano/plus.con x y).
110 interpretation 'mult x y = (cic:/Coq/Init/Peano/mult.con x y).
111 render cic:/Coq/Arith/Mult/mult_plus_distr_r.con.
113 notation \[ \TERM a \OVER \TERM b : \TERM c \SQRT \TERM d \] for 'megacoso \TERM a \TERM b \TERM c \TERM d.
114 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)).
115 render cic:/Coq/Arith/Plus/plus_comm.con.
119 notation \[ \TERM a + \TERM b \] for 'plus \TERM a \TERM b.
121 interpretation 'plus x y = (cic:/Coq/Init/Peano/plus.con x y).
122 render cic:/Coq/Arith/Plus/plus_comm.con.
124 notation \[ \TERM a + \TERM b \] left associative with precedence 50 for 'plus \TERM a \TERM b.
125 notation \[ \TERM a * \TERM b \] left associative with precedence 60 for 'mult \TERM a \TERM b.
126 interpretation 'plus x y = (cic:/Coq/Init/Peano/plus.con x y).
127 interpretation 'mult x y = (cic:/Coq/Init/Peano/mult.con x y).
128 render cic:/Coq/Arith/Mult/mult_plus_distr_r.con.
130 notation \[ \LIST \NUM a \] for \FOLD left \[ 'a \] \LAMBDA acc \[ 'b \NUM a \].