Hi, I'm working on a MetaCoq implementation of the Coq guardedness checker. As part of that, I have changed the MC representation of inductives to incorporate the recargs tree for inductive bodies (what corresponds to mind_recargs
in the OCaml impl).
Of course, that also requires adding that to TemplateCoq's quoting mechanism. I've changed the quoting functions to quote the wf_paths when quoting inductive bodies.
However, I'm having trouble with adding the right references to the Coq term constructors in src/constr_reification.ml
. Since the type wf_paths
is available in theories/Ast.v
under that name, I thought that let twf_paths = ast "wf_paths"
in src/constr_reification.ml
would be the right thing.
But when using this for quoting in Coq, I get Error: not found in table: metacoq.ast.wf_paths
.
So in short, I suppose my assumptions about how the lookup mechanism for the Coq names works are wrong.
Can someone please push me in the right direction? Where do I need to look to find out the right names I need to use in src/constr_reification.ml
to reference my new Coq type?
You probably need the Register command, search the code for other uses to see how it's used
You need to register them in template-coq/theories/Constants.v
indeed
Thanks a lot, that made it work
Last updated: Oct 13 2024 at 01:02 UTC