Jason Gross (Feb 14 2023 at 21:24): Jason Gross (Feb 14 2023 at 21:24):Is there a primitive for (parallel) substituting a (list of) rel(s) for a (list of) identifier(s)? (I want to build a template program that takes in a list of modules, does tmQuoteModule to get all the constants in the modules, and then emits versions of the definitions / inductives that take as arguments any MPbound identifiers)
Yannick Forster (Feb 14 2023 at 21:26):Do you want a function where the output has less tRels, or more? (I think one can read what your asking in two different ways)
Jason Gross (Feb 14 2023 at 21:28):More. I want to replace tVar with tRel
Last updated: Jun 04 2023 at 23:30 UTC