Stream: Elpi users & devs

Topic: Parens / command parsing

Gordon Stewart (Jan 20 2022 at 18:47):

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?

Enrico Tassi (Jan 20 2022 at 19:08):

As of today you can't. The doc is here: https://github.com/LPCIC/coq-elpi/#invocation-of-elpi-code

Enrico Tassi (Jan 20 2022 at 19:09):

One way of not having to put parentheses is to take in input a Coq declaration (which is parsed using the usual Coq syntax).

Enrico Tassi (Jan 20 2022 at 19:10):

Your nat was parsed as a string, hence (str "nat"). Depending on what you want to do, that would be enough or not.

Gordon Stewart (Jan 20 2022 at 21:20):

I see. I missed that particular doc. Thanks!

Last updated: Oct 13 2024 at 01:02 UTC