no viable alternative error for Gobra keywords not allowed in Go code

[lmeinen]

The following code

package bar

func foo() {
	match := 1
}

throws the following error in v23.02

no viable alternative at input 'match :='
	match := 1
 ^^^^^^^^^^

Similar errors occur for other Gobra keywords, e.g. proof, domain, requires, etc.

Expected behavior would of course be that Gobra keywords are allowed within Go code. As a second option, it would be nice if the error were more descriptive. Note that this is the same error one gets when verifying invalid Gobra code directly, e.g.

package bar

requires
func foo() {
	someVar := 1
}

results in

no viable alternative at input 'func'
func foo() {
^^^^^^^^^^^^