X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Flib%2Farith.ma;h=1ba525475622dfe3fb6777c4cbe59847a4584a1d;hb=5832735b721c0bd8567c8f0be761a9136363a2a6;hp=325e07d387be02cc1c321016b426b5da69d03e63;hpb=064980eacc2efe70ffee96134d75dfa37506fc36;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
index 325e07d38..1ba525475 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
@@ -220,7 +220,7 @@ qed-.
 (* Iterators ****************************************************************)
 
 (* Note: see also: lib/arithemetics/bigops.ma *)
-let rec iter (n:nat) (B:Type[0]) (op: B → B) (nil: B) ≝
+rec definition iter (n:nat) (B:Type[0]) (op: B → B) (nil: B) ≝
   match n with
    [ O   ⇒ nil
    | S k ⇒ op (iter k B op nil)
@@ -249,7 +249,7 @@ qed.
 (* Trichotomy operator ******************************************************)
 
 (* Note: this is "if eqb n1 n2 then a2 else if leb n1 n2 then a1 else a3" *)
-let rec tri (A:Type[0]) n1 n2 a1 a2 a3 on n1 : A ≝
+rec definition tri (A:Type[0]) n1 n2 a1 a2 a3 on n1 : A ≝
   match n1 with
   [ O    ⇒ match n2 with [ O ⇒ a2 | S n2 ⇒ a1 ]
   | S n1 ⇒ match n2 with [ O ⇒ a3 | S n2 ⇒ tri A n1 n2 a1 a2 a3 ]