mm0 parser wrongly accepts dummy binders in "theorem"

[Lakedaemon]

in mm0.md, The grammar of theorem uses

assert-stmt ::= ('axiom' | 'theorem') identifier (formula-type-binder) ':' formula-arrow-type ';' formula-type-binder ::= '{' (identifier) ':' type '}' | '(' (identifier_)* ':' (type | formula) ')' yet mm0.mm0 uses dummy variable like in theorem ProofThm (env e p a h r .p1 .ds .pf .ctx: nat):

You probably meant axiom and theorems to be able to use dummy variables and so, maybee thos binders should be uesd :

dummy-binder ::= '{' (dummy-identifier) ':' type '}' | '(' (dummy-identifier) ':' type ')' dummy-identifier ::= '.' identifier | identifier_

[digama0]

Axiom and theorem do not take dummy variables. Alternatively, the spec could be modified to allow them, but they have no effect. This is because unlike definitions, axioms and theorems have no = clause, so there is no need for bound variables that appear in the proof but not the statement. (For bound variables that appear in the statement, you use the regular curly binder {x: nat}.)

[Lakedaemon]

ok, then could you please fix the mm0.mm0 file.

Because the parse for `theorem ProofThm (env e p a h r .p1 .ds .pf .ctx: nat): should be illegal for the current grammar (there are 4 dummy variables in the formula-type-binder that doesn't allow dummy variables that start with '.')

I'll open source the kotlin mm0 parser/verifier. But I need legal mm0 files to test it agains. Also, could you send me a translated .mm0 file for set.mm (to also test my kotlin mm0 parser and the futurekotlin mm0 verifier) ? It is a hassle to build stuff with haskel without instructions and sadly, I don't have much time to fool around.

[digama0]

Oh! Now I see your point. All of those variables should be in curly binders and should not be dummies. Will fix. (I also need to fix my parser, which should have rejected it.)

[Lakedaemon]

thanks :) Also, thank you for confirming that the grammar spec was correct :)

[digama0]

fixed in f1bc737