Dafny: allowed strictly finite datatypes in comprehensions, quantifiers, and parallel statements.

1 files changed, 6 insertions, 0 deletions

diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs
index 61df448f..ac688143 100644
--- a/Binaries/DafnyRuntime.cs
+++ b/Binaries/DafnyRuntime.cs
@@ -509,6 +509,12 @@ namespace Dafny
       }

       return frall;

     }

+    public static bool QuantDatatype<U>(IEnumerable<U> set, bool frall, System.Predicate<U> pred) {

+      foreach (var u in set) {

+        if (pred(u) != frall) { return !frall; }

+      }

+      return frall;

+    }

     // Enumerating other collections

     public delegate Dafny.Set<T> ComprehensionDelegate<T>();

     public delegate Dafny.Map<U, V> MapComprehensionDelegate<U, V>();