Let's say I have
Elpi Command Parens. Elpi Accumulate " main [str TermName, str "":"", trm Ty] :- coq.say ""Term"" TermName "":"" Ty. ". Elpi Typecheck. Elpi Export Parens.
I'd expect the following to work:
Parens x : nat.
but it gives
Error: The elpi command Parens failed without giving a specific error message. Please report this inconvenience to the authors of the program.
Instead, I have to write:
Parens x : (nat).
with the parens.
Am I missing something obvious? What can I do (if anything) to get the no-parens parsing behavior?
As of today you can't. The doc is here: https://github.com/LPCIC/coq-elpi/#invocation-of-elpi-code
One way of not having to put parentheses is to take in input a Coq declaration (which is parsed using the usual Coq syntax).
nat was parsed as a string, hence
(str "nat"). Depending on what you want to do, that would be enough or not.
I see. I missed that particular doc. Thanks!
Last updated: Jun 06 2023 at 22:01 UTC