diff options
| author |  leino <unknown> | 2015-05-11 01:03:03 -0700 |
|---|---|---|
| committer | leino <unknown> | 2015-05-11 01:03:03 -0700 |
| commit | b07a96a9dca143fe669fc464dd36fee2a100d2ce (patch) | |
| tree | 476d184d72c58af0271c36b998a86cf0c3431ea4 /Test/dafny4/NipkowKlein-chapter3.dfy | |
| parent | 2e88568000690f3b5e79069e0fdcba5fef8f5ca9 (diff) | |
Don't include arrow types among ordered types.
Fix bug with not seeing imap's because of type synonyms.
Don't show semi-colon after "decreases" in hover text.
Minor cosmetic change in a test case.
Diffstat (limited to 'Test/dafny4/NipkowKlein-chapter3.dfy')
| -rw-r--r-- | Test/dafny4/NipkowKlein-chapter3.dfy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/dafny4/NipkowKlein-chapter3.dfy b/Test/dafny4/NipkowKlein-chapter3.dfy index 024ef9bd..6572359a 100644 --- a/Test/dafny4/NipkowKlein-chapter3.dfy +++ b/Test/dafny4/NipkowKlein-chapter3.dfy @@ -41,7 +41,7 @@ function aval(a: aexp, s: state): val match a
case N(n) => n
case V(x) => s(x)
- case Plus(a0, a1) => aval(a0,s ) + aval(a1, s)
+ case Plus(a0, a1) => aval(a0, s) + aval(a1, s)
}
lemma Example0()
|