From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 25 May 2005 15:11:59 +0000 (+0000)
Subject: let rec example
X-Git-Tag: PRE_INDEX_1~124
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fa12508ec9af00a9182e30d747884c0425a807c3;p=helm.git

let rec example
---

diff --git a/helm/matita/tests/letrec.ma b/helm/matita/tests/letrec.ma
new file mode 100644
index 000000000..6712765aa
--- /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.
+