]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_plus.ma
- new syntax for let rec/corec with flavor specifier (tested on lambdadelta/ground_2/)
[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / relocation / mr2_plus.ma
index 11ffaa40710a4b7d9b848e07601974aa139c37af..da3380da9cb9a740efc8aaa70478622242085f5b 100644 (file)
@@ -16,7 +16,7 @@ include "ground_2/relocation/mr2.ma".
 
 (* MULTIPLE RELOCATION WITH PAIRS *******************************************)
 
-let rec pluss (cs:mr2) (i:nat) on cs ≝ match cs with
+rec definition pluss (cs:mr2) (i:nat) on cs ≝ match cs with
 [ nil2         ⇒ ◊
 | cons2 l m cs ⇒ {l + i, m} @ pluss cs i
 ].