summaryrefslogtreecommitdiff
path: root/Source/DafnyExtension
diff options
context:
space:
mode:
authorGravatar Rustan Leino <unknown>2014-01-06 23:38:06 -0800
committerGravatar Rustan Leino <unknown>2014-01-06 23:38:06 -0800
commit40bd1796bd385a9d04d8a94259441817ef1b4977 (patch)
tree00f18c345937c219925b9a890c75ee681cd78641 /Source/DafnyExtension
parent9ae6866cad0c6af00010940013e1ed272c649e77 (diff)
One more file to go with the previous check-in (DafnyRuntime.cs apparently gets copied)
Diffstat (limited to 'Source/DafnyExtension')
-rw-r--r--Source/DafnyExtension/DafnyRuntime.cs9
1 files changed, 9 insertions, 0 deletions
diff --git a/Source/DafnyExtension/DafnyRuntime.cs b/Source/DafnyExtension/DafnyRuntime.cs
index a8faafae..f61163d0 100644
--- a/Source/DafnyExtension/DafnyRuntime.cs
+++ b/Source/DafnyExtension/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) {