diff options
| author |  Dan Rosén <danr@chalmers.se> | 2014-08-11 16:07:38 -0700 |
|---|---|---|
| committer | Dan Rosén <danr@chalmers.se> | 2014-08-11 16:07:38 -0700 |
| commit | 8797f054f44d114147562689d80c9970d8ea4f82 (patch) | |
| tree | 6a9e99a6a39126f946c0e7dd55cf0fa03a1a0ca7 /Source/DafnyExtension | |
| parent | 4cbe4583b329a39dee2b4b456758cafbe7e2fa79 (diff) | |
| parent | 08ab990d6f1a188c6cc039d6a2289daf41ff52d3 (diff) | |
Merge
Diffstat (limited to 'Source/DafnyExtension')
| -rw-r--r-- | Source/DafnyExtension/DafnyRuntime.cs | 7 | ||||
| -rw-r--r-- | Source/DafnyExtension/TokenTagger.cs | 2 |
2 files changed, 9 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>
diff --git a/Source/DafnyExtension/TokenTagger.cs b/Source/DafnyExtension/TokenTagger.cs index 5068354a..438d9be6 100644 --- a/Source/DafnyExtension/TokenTagger.cs +++ b/Source/DafnyExtension/TokenTagger.cs @@ -284,6 +284,8 @@ namespace DafnyLanguage case "calc":
case "case":
case "class":
+ case "trait":
+ case "extends":
case "codatatype":
case "colemma":
case "constructor":
|