let rec example

diff --git a/helm/matita/tests/letrec.ma b/helm/matita/tests/letrec.ma
new file mode 100644 (file)
index 0000000..6712765
--- /dev/null
+++ b/helm/matita/tests/letrec.ma
@@ -0,0 +1,9 @@
+
+definition plus: nat \to nat \to nat \def
+  let rec plus (n,m:nat) \def
+    match n with
+    [ O \Rightarrow m
+    | (S x) \Rightarrow S (plus x m) ]
+  in
+  plus.
+