I wrote a function
quote_term : MetaCoq.Template.Ast.term -> MetaCoq.Template.Ast.term which adds a level of quotation (https://github.com/JasonGross/metacoq-lob/blob/e9703eee66f2431654d659bf8d7b8bb63fc99e91/theories/QuoteGround.v#L100). I'm looking to do the same thing with
MetaCoq.PCUIC.PCUICAst.term instead (and eventually with complete typing judgments; I'm working up to Lob's theorem). Is there any tactic / tactic monad / notation support for using the PCUIC AST, or do I have manually map everything though
TemplateToPCUIC.trans or something?
Is there a version of the template monad's tmQuote (and tmUnquote) that works on PCUIC?
Nope, you have to go through the translation
But that's fairly easy to program I guess
The translation requires access to a
PCUICProgram.global_env_map. Is there an easy way to manifest one with all the required inductives?
(I'm currently in the process of trying to write a version of
trans that doesn't take such a map and instead lives inside the template monad. (Perhaps this would be worth merging upstream, if there's not already an easy alternative?))
You can easily build a global_env_map out of a global env using
I guess you found that
Last updated: Feb 04 2023 at 03:30 UTC