Hello. I got this error today while trying to print a Coq term:
What is this case exactly? Is it because the fixpoint I wanted to quote has several arguments?
IIUC, Coq has 3 ASTs, one for parsing, the global AST is the second one, with names elaborated to their full paths and notations resolved, and the
constr thing is the fully-typed one in the kernel. So I wanted to ask why do we need this
gterm2lp API? As we already have
constr2lp. I thought that one might just let Coq do the first parsing phase then only implement the quote and unquote operations on
Terms passed to an elpi command are not typechecked yet, unlike the ones you pull from the env.
You probably passed a fix with no struct annotation (saying which the recursive argument is).
A more descriptive error message would be better I guess.
FTR Coq has 3 AST:
Elpi only gives you one, hence
I believe it is a mistake to have globterms even in Coq, but it is hard to get rid of foe technical reasons
In particular the "elborator" (pretyper) goes from glob -> constr, which makes it not compose with itself, so we have another typechecker from constr -> constr which you use after the first step...
Thanks for the information.
I do want elpi commands to take raw (un-elaborated) terms to give them more freedom:
I added the struct annotation and the problem is solved. Now it's the match that fails. But it's not a big deal, I just wanted to see what a term looked like in Elpi in order to learn how
match are implemented in HOAS. I'll have a look somewhere else or with a simpler term.
The match must be simple, on one term and not deep
fetch Nat.plus for the env and print it, it is what I do in the tutorials
Last updated: Jun 06 2023 at 23:01 UTC