summaryrefslogtreecommitdiff
path: root/Binaries/DafnyRuntime.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Binaries/DafnyRuntime.cs')
-rw-r--r--Binaries/DafnyRuntime.cs13
1 files changed, 13 insertions, 0 deletions
diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs
index d1a3c092..4dda19fe 100644
--- a/Binaries/DafnyRuntime.cs
+++ b/Binaries/DafnyRuntime.cs
@@ -1012,6 +1012,12 @@ namespace Dafny
return pred(false) || pred(true);
}
}
+ public static bool QuantChar(bool frall, System.Predicate<char> pred) {
+ for (int i = 0; i < 0x10000; i++) {
+ if (pred((char)i) != frall) { return !frall; }
+ }
+ return frall;
+ }
public static bool QuantInt(BigInteger lo, BigInteger hi, bool frall, System.Predicate<BigInteger> pred) {
for (BigInteger i = lo; i < hi; i++) {
if (pred(i) != frall) { return !frall; }
@@ -1051,6 +1057,13 @@ namespace Dafny
yield return true;
}
}
+ public static IEnumerable<char> AllChars {
+ get {
+ for (int i = 0; i < 0x10000; i++) {
+ yield return (char)i;
+ }
+ }
+ }
public static IEnumerable<BigInteger> AllIntegers {
get {
yield return new BigInteger(0);