X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Faplus%2Fdefs.ma;h=f339331a642a51396fdbb36bddf90451d9544caf;hb=57ae1762497a5f3ea75740e2908e04adb8642cc2;hp=c26b3c28656754bb6898772e31b1c451ebf19620;hpb=639e798161afea770f41d78673c0fe3be4125beb;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/aplus/defs.ma b/matita/matita/contribs/lambdadelta/basic_1/aplus/defs.ma
index c26b3c286..f339331a6 100644
--- 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 (asucc g (aplus g a n0))].
+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))].