diff options
| author |  Rustan Leino <unknown> | 2014-03-17 15:16:16 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-03-17 15:16:16 -0700 |
| commit | e4e919490ff161bd7acaa81b8c5bca49b719c58e (patch) | |
| tree | 3b5bd33435176c2e68ed63acb0ac30860502a9ff /Test/dafny4/NumberRepresentations.dfy | |
| parent | b4648bc600a7f566aa150864950a6385ce3bd9af (diff) | |
AST refactoring:
Changed VarDecl to no longer inherit from Statement.
Removed ConcreteSyntaxStatement and changed VarDeclStmt's superclass be Statement.
Diffstat (limited to 'Test/dafny4/NumberRepresentations.dfy')
| -rw-r--r-- | Test/dafny4/NumberRepresentations.dfy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/dafny4/NumberRepresentations.dfy b/Test/dafny4/NumberRepresentations.dfy index 2f31c006..b8c261d7 100644 --- a/Test/dafny4/NumberRepresentations.dfy +++ b/Test/dafny4/NumberRepresentations.dfy @@ -77,7 +77,7 @@ lemma CompleteNat(n: nat, base: nat) returns (digits: seq<int>) base * n <= n;
(base - 1) * n + n <= n;
(base - 1) * n <= 0;
- ==> { MulSign(base - 1, n); }
+ ==> { assert (base - 1) * n <= 0; MulSign(base - 1, n); }
(base - 1) <= 0 || n <= 0;
{ assert 0 < n; }
(base - 1) <= 0;
|