+
+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
+