Dafny: added optional range expressions to logical quantifiers, preparing for addition other other comprehensions (like set comprehension)

1 files changed, 7 insertions, 2 deletions

diff --git a/Dafny/Printer.cs b/Dafny/Printer.cs
index 003a977c..6dcf0020 100644
--- a/Dafny/Printer.cs
+++ b/Dafny/Printer.cs
@@ -931,14 +931,19 @@ namespace Microsoft.Dafny {
         wr.Write(" ");

         PrintAttributes(e.Attributes);

         PrintTriggers(e.Trigs);

+        if (e.Range != null) {

+          wr.Write("| ");

+          PrintExpression(e.Range);

+          wr.Write(" ");

+        }

         wr.Write(":: ");

         if (0 <= indent) {

           int ind = indent + IndentAmount;

           wr.WriteLine();

           Indent(ind);

-          PrintExpression(e.Body, ind);

+          PrintExpression(e.Term, ind);

         } else {

-          PrintExpression(e.Body);

+          PrintExpression(e.Term);

         }

         if (parensNeeded) { wr.Write(")"); }