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 | |
| 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.
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 2 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 1 | ||||
| -rw-r--r-- | Test/dafny4/NipkowKlein-chapter3.dfy | 2 |
3 files changed, 2 insertions, 3 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 83da7598..99dfecd6 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -633,7 +633,7 @@ namespace Microsoft.Dafny { /// </summary>
public bool IsOrdered {
get {
- return !IsTypeParameter && !IsCoDatatype && !(this is MapType && ((MapType)this).Finite);
+ return !IsTypeParameter && !IsCoDatatype && !IsArrowType && !IsIMapType;
}
}
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index f334fc4d..f7ec135b 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -495,7 +495,6 @@ namespace Microsoft.Dafny sep = ", ";
}
}
- s += ";"; // always terminate with a semi-colon, even in the case of an empty decreases clause
// Note, in the following line, we use the location information for "clbl", not "m". These
// are the same, except in the case where "clbl" is a CoLemma and "m" is a prefix lemma.
ReportAdditionalInformation(clbl.Tok, s, clbl.Tok.val.Length);
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()
|