Fix issue 94. Allow tuple-based assignment in statement contexts.

1 files changed, 8 insertions, 0 deletions

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 2786133e..82795480 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -1764,6 +1764,14 @@ namespace Microsoft.Dafny {
           wr.Write(TrStmt(s.Update, indent).ToString());

         }

 

+      } else if (stmt is LetStmt) {

+        var s = (LetStmt)stmt;

+        for (int i = 0; i < s.LHSs.Count; i++) {

+          var lhs = s.LHSs[i];

+          if (Contract.Exists(lhs.Vars, bv => !bv.IsGhost)) {

+            TrCasePatternOpt(lhs, s.RHSs[i], null, indent, wr, false);

+          }

+        }

       } else if (stmt is ModifyStmt) {

         var s = (ModifyStmt)stmt;

         if (s.Body != null) {