Stream: MetaCoq

Topic: global_reference -> term in the template monad

view this post on Zulip Jason Gross (Feb 14 2023 at 02:35):

Is there a way to generate a fresh instance (or to at least determine how many universe parameters a global reference has)? (I want to write some automation that takes a module name M and for every definition M.d emits #[export] Instance qd : quotation_of M.d := <% M.d %>. and for every inductive M.ind emits #[export] Instance qind : inductive_quotation_of M.ind := Build_inductive_quotation_of <the inductive for M.ind> <a fresh instance for M.ind>.

For now I guess I'm going to make everything monomorphic, but it would be nice to have the automation also work for polymorphic things.

Last updated: Jun 03 2023 at 18:01 UTC