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 4095b163bfcd0b9c3beb78207cfd38e72ab42bd2..f339331a642a51396fdbb36bddf90451d9544caf 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/aplus/defs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/aplus/defs.ma
@@ -14,11 +14,8 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/asucc/defs.ma".
+include "basic_1/asucc/defs.ma".
 
-definition aplus:
- G \to (A \to (nat \to A))
-\def
- 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))]) in aplus.
+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))].