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
#[export] Instance qd : quotation_of M.d := <% M.d %>. and for every inductive
#[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