misalignment of documentation with parser (python)
Hi everyone, in Section 9.2.1, Syntax of micro-Python, of the manual (https://why3.lri.fr/doc/input_formats.html#syntax-of-micro-python) the logic declaration of a function is defined as:
logic_declaration ::= "#@" "function" identifier "(" params ")" return_type? ("variant" "{" term "}")? ("=" term)? NEWLINE
However, in the parser (file why3/plugins/python/py_parser.mly on gitlab), the corresponding rule for fp_variant is (line 155):
LEFTBR VARIANT v=term RIGHTBR { v }
i.e., the documentation says to write it variant { n } and the parser awaits { variant n }.
Bests,
Yannick