]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma
- new syntax for let rec/corec with flavor specifier (tested on lambdadelta/ground_2/)
[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / relocation / nstream.ma
index 8d7dacc4ed7632a7270f33473076f238b6c20601..c852317f895c60e34fc403dd6f7c2572bc0a3620 100644 (file)
@@ -25,7 +25,7 @@ interpretation "push (nstream)" 'Lift f = (push f).
 
 definition next: rtmap → rtmap.
 * #n #f @(⫯n@f)
-qed.
+defined.
 
 interpretation "next (nstream)" 'Successor f = (next f).