Jason Gross (Oct 17 2022 at 10:57): Jason Gross (Oct 17 2022 at 10:57):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?
Jason Gross (Oct 18 2022 at 09:56):Is there a version of the template monad's tmQuote (and tmUnquote) that works on PCUIC?
Matthieu Sozeau (Oct 18 2022 at 11:04):Nope, you have to go through the translation
Matthieu Sozeau (Oct 18 2022 at 11:04):But that's fairly easy to program I guess
Jason Gross (Oct 18 2022 at 13:38):The translation requires access to a PCUICProgram.global_env_map. Is there an easy way to manifest one with all the required inductives?
Jason Gross (Oct 18 2022 at 13:38):(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?))
Matthieu Sozeau (Nov 23 2022 at 12:22):You can easily build a global_env_map out of a global env using PCUICProgram.build_global_env_map
Matthieu Sozeau (Nov 23 2022 at 12:22):I guess you found that
Last updated: Feb 04 2023 at 03:30 UTC