Co-recursion, now sounder than ever!

- prefix equality is destructive
- co-methods are not allowed to have out-parameters
- in an SCC with both co-recursive and recursive calls, the latter are allowed only in non-destructive contexts

1 files changed, 2 insertions, 1 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 0aac1cd6..b58f392c 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -3933,7 +3933,8 @@ namespace Microsoft.Dafny {
       NoBecauseFunctionHasSideEffects,

       NoBecauseFunctionHasPostcondition,

       NoBecauseRecursiveCallsAreNotAllowedInThisContext,

-      NoBecauseIsNotGuarded

+      NoBecauseIsNotGuarded,

+      NoBecauseRecursiveCallsInDestructiveContext

     }

     public CoCallResolution CoCall = CoCallResolution.No;  // indicates whether or not the call is a co-recursive call; filled in by resolution