usage with comments in a .go file?

[gregwebs]

It would be easier to try this project out if instead of a .gobra file one could put the gobra extension into comments so the file could still be used as a regular .go file.

[ArquintL]

Hi Greg,
Thanks for your interest in Gobra. While we support verifying .go files, it is indeed unfortunate that this is not yet reflected in the tutorial.
If you put your specification into so-called specification comments, Gobra will consider them in .go files. Specification comments either start with //@ or are delimited by /*@ and @*/. Also note that you can optionally add a whitespace before/after the @ sign to be compliant with comments in Go >= 1.19