summaryrefslogtreecommitdiff
path: root/Binaries/DafnyRuntime.cs
diff options
context:
space:
mode:
authorGravatar Rustan Leino <unknown>2014-01-08 18:48:40 -0800
committerGravatar Rustan Leino <unknown>2014-01-08 18:48:40 -0800
commitecb53212d30f7e8ef6145bcca9f40517e1999956 (patch)
tree7312d15fd2974850a09a027efce2fbd8220f8e6d /Binaries/DafnyRuntime.cs
parent041a1a226a96ba55ff22251eb98666241a1d769a (diff)
parentdd82ee5e33d25f6a5570da2ad6ab650ce6dc3164 (diff)
Merge
Diffstat (limited to 'Binaries/DafnyRuntime.cs')
-rw-r--r--Binaries/DafnyRuntime.cs9
1 files changed, 9 insertions, 0 deletions
diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs
index 3afac587..2d033b0d 100644
--- a/Binaries/DafnyRuntime.cs
+++ b/Binaries/DafnyRuntime.cs
@@ -581,6 +581,15 @@ namespace Dafny
yield return true;
}
}
+ public static IEnumerable<BigInteger> AllIntegers {
+ get {
+ yield return new BigInteger(0);
+ for (var j = new BigInteger(1);; j++) {
+ yield return j;
+ yield return -j;
+ }
+ }
+ }
// pre: b != 0
// post: result == a/b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)
public static BigInteger EuclideanDivision(BigInteger a, BigInteger b) {