- new syntax for let rec/corec with flavor specifier (tested on lambdadelta/ground_2/)

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / gcp_cr.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_cr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_cr.ma
index dc9c4498eceb70d7f4830e3f7b60d4bd3eef5de1..b60a87aef07f9d933e3dc3591a9ac35b49edc340 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_cr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_cr.ma
@@ -66,7 +66,7 @@ definition cfun: candidate → candidate → candidate ≝
                  ⬇*[Ⓕ, cs] L ≡ K → ⬆*[cs] T ≡ U → C1 G L W → C2 G L (ⓐW.U).
 
 (* the reducibility candidate associated to an atomic arity *)
-let rec acr (RP:candidate) (A:aarity) on A: candidate ≝
+rec definition acr (RP:candidate) (A:aarity) on A: candidate ≝
 match A with
 [ AAtom     ⇒ RP
 | APair B A ⇒ cfun (acr RP B) (acr RP A)