notation \[ \TERM a ++ \OPT \NUM i \] for 'assign \TERM a ('plus \TERM a \DEFAULT \[\NUM i\] \[1\]).
# sample mappings level 1 <--> level 2
notation \[ \TERM a ++ \OPT \NUM i \] for 'assign \TERM a ('plus \TERM a \DEFAULT \[\NUM i\] \[1\]).
-print 1 ++ 2.
+check 1 ++ 2.
notation \[ + \LIST0 \NUM a \] for \FOLD right \[ 'zero \] \LAMBDA acc \[ 'plus \NUM a \TERM acc \].
notation \[ + \LIST0 \NUM a \] for \FOLD right \[ 'zero \] \LAMBDA acc \[ 'plus \NUM a \TERM acc \].
-print + 1 2 3 4.
+check + 1 2 3 4.
notation \[ [ \HOVBOX\[ \LIST0 \TERM a \SEP ; \] ] \] for \FOLD right \[ 'nil \] \LAMBDA acc \[ 'cons \TERM a \TERM acc \].
notation \[ [ \HOVBOX\[ \LIST0 \TERM a \SEP ; \] ] \] for \FOLD right \[ 'nil \] \LAMBDA acc \[ 'cons \TERM a \TERM acc \].
-print [].
-print [1;2;3;4].
+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) \] .
notation \[ [ \LIST0 \[ \TERM a ; \TERM b \] \SEP ; ] \] for \FOLD right \[ 'nil \] \LAMBDA acc \[ 'cons \TERM a ( 'cons \TERM b \TERM acc) \] .
-print [].
-print [1;2].
-print [1;2;3;4].
+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 \[ \TERM a \OPT \[ , \TERM b \] \] \SEP ; | \] for \FOLD right \[ 'nil \] \LAMBDA acc \[ 'cons \DEFAULT \[ \TERM a \] \[ ('pair \TERM a \TERM b) \] \TERM acc \] .
@@ -106,13+114,17 @@ 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.
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 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)).
+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.
render cic:/Coq/Arith/Plus/plus_comm.con.
# full samples
notation \[ \TERM a + \TERM b \] for 'plus \TERM a \TERM b.
-print 1 + 2.
+check 1 + 2.
interpretation 'plus x y = (cic:/Coq/Init/Peano/plus.con x y).
render cic:/Coq/Arith/Plus/plus_comm.con.
interpretation 'plus x y = (cic:/Coq/Init/Peano/plus.con x y).