Open MikaelMayer opened 2 weeks ago
We now have some IDE (play icon) and CLI options (--filter-symbol
/--filter-position
) to verify specific things. What's still missing from the IDE is an option to verify individual assertions.
However, once we have that, is there still a use-case for {:only}
? To me the act of making source changes to help development does not seem like a good UX, and can even be unsafe when those changes are accidentally committed.
Dafny version
latest-nightly
Code to produce this issue
Command to run and resulting output
What happened?
Four issues there:
{:only}
is not mentioned in VSCode, only on the command-line.What type of operating system are you experiencing the problem on?
Windows