diff options
| author |  leino <unknown> | 2014-08-02 01:05:17 -0700 |
|---|---|---|
| committer | leino <unknown> | 2014-08-02 01:05:17 -0700 |
| commit | ae578ae92040975fed005d045110679e4e858c31 (patch) | |
| tree | 79f2a3a67c8c9059a89d9771e933c8a0b6b601bf /Source/DafnyExtension | |
| parent | 54b670417f5974c43ef2fd55d37ba3806ad5c72d (diff) | |
Fixed bug Issue 37: expand type synonyms in more (hopefully all) places in the resolver and translator
Diffstat (limited to 'Source/DafnyExtension')
| -rw-r--r-- | Source/DafnyExtension/DafnyRuntime.cs | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/Source/DafnyExtension/DafnyRuntime.cs b/Source/DafnyExtension/DafnyRuntime.cs index 6f0cab13..d6bd895a 100644 --- a/Source/DafnyExtension/DafnyRuntime.cs +++ b/Source/DafnyExtension/DafnyRuntime.cs @@ -656,6 +656,13 @@ namespace Dafny num = n;
den = d;
}
+ public BigInteger ToBigInteger() {
+ if (0 <= num) {
+ return num / den;
+ } else {
+ return (num - den + 1) / den;
+ }
+ }
/// <summary>
/// Returns values such that aa/dd == a and bb/dd == b.
/// </summary>
|