]> matita.cs.unibo.it Git - helm.git/blob - helm/matita/tests/letrec.ma
added Variant theorem flavour
[helm.git] / helm / matita / tests / letrec.ma
1 set "baseuri" "cic:/matita/tests/letrec/".
2
3
4 alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)".
5 alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)".
6 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
7
8 let rec plus n m \def
9  match n with
10   [ O \Rightarrow m
11   | (S x) \Rightarrow S (plus x m) ].