update in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_1 / aplus / defs.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_1/aplus/defs.ma b/matita/matita/contribs/lambdadelta/basic_1/aplus/defs.ma
index 08c752cb8718616cf5308be1fa6f7e17f3acc888..f339331a642a51396fdbb36bddf90451d9544caf 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/aplus/defs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/aplus/defs.ma
@@ -16,6 +16,6 @@
 
 include "basic_1/asucc/defs.ma".
 
-let rec aplus (g: G) (a: A) (n: nat) on n: A \def match n with [O \Rightarrow 
-a | (S n0) \Rightarrow (let TMP_1 \def (aplus g a n0) in (asucc g TMP_1))].
+rec definition aplus (g: G) (a: A) (n: nat) on n: A \def match n with [O 
+\Rightarrow a | (S n0) \Rightarrow (asucc g (aplus g a n0))].