The emacs mode for Dafny visualizes Dafny's forall keyword in two different ways. For forall expressions (that is, universal quantifications), it visualizes the keyword as an ∀. For forall statements it (mostly) visualizes the keyword as itself (forall). Which one to choose is, I believe, determined by a simple syntactic scan of some things that follow the forall keyword. Here is one case where that simple scan makes the wrong determination, which I think can easily be improved.
When the ensures clause happens on the subsequent line, all is good:
forall x: int | true
ensures Ǝ y :: x == y
{
}
But when the first line contains a :: (even if there's an ensures in between), then the forall turns into a ∀:
∀ x: int | true ensures Ǝ y :: x == y {
}
It would seem that the syntactic scan could look for an ensures. If it finds an ensures before it finds a ::, then the preceding forall is probably a forall statement.
The emacs mode for Dafny visualizes Dafny's
forallkeyword in two different ways. Forforallexpressions (that is, universal quantifications), it visualizes the keyword as an ∀. Forforallstatements it (mostly) visualizes the keyword as itself (forall). Which one to choose is, I believe, determined by a simple syntactic scan of some things that follow theforallkeyword. Here is one case where that simple scan makes the wrong determination, which I think can easily be improved.When the
ensuresclause happens on the subsequent line, all is good:But when the first line contains a
::(even if there's anensuresin between), then theforallturns into a ∀:It would seem that the syntactic scan could look for an
ensures. If it finds anensuresbefore it finds a::, then the precedingforallis probably aforallstatement.