James "kjx" Noble

forall statement and expression syntax gratuitously inconsistent -> horrible error messages LOW SEVERITY

4

### Dafny version 4.6.0 ### Code to produce this issue ```dafny forall x 10 by { reveal someRandomThing(); } ///yes I have lots of these things. ///yes they take up...

non-non-non-optional semicolons give horrible error messages - LOW SEVERITY

3

### Dafny version 4.6.0 ### Code to produce this issue ```dafny method Main() { assert 3 == 3 by { true; }; } ``` ### Command to run and resulting...

assertion of map values fails when same postcondition succeeds (or if preceded by Keys assertion)

2

### Dafny version 4.6.0.0 nightly ### Code to produce this issue ```dafny class Object {} method ISSUE( rm : map, a : Object, b : Object, context : set) returns...

### Summary I can write assert FOO: forall x

### Summary assume FOO: x == 4; //doesn't work ### Background and Motivation doing something to complex and wrongly ### Proposed Feature being able to label assumptions in exactly the...

### Summary (sorry couldn't resist the issue title) the dafny command needs better help ### Background and Motivation running the dafny command gets an informative message: ``` .dafny Required command...