I would like to have a tactic that takes e.g. a constructor
C of an inductive
Iand gives me the reified definition of this inductive. My goal is to retrieve some information about the inductive
I, for instance, the number of mutual inductive in
I, the name of all other constructors etc.
Basically, among other things, I would need to have a
MetaCoq Quote Recursivelyversion of the tactic below (which suggested to me by @Yannick Forster some time ago):
Ltac pose_quoted_term c idn :=
let X := c in quote_term X ltac:(fun Xast => pose Xast as idn).
Is there a way to do this in the current version of
Instead of quote_term you should be able to use the run_template_program tactic and then use tmQuoteRec
OK, thanks one more time Yannick :)
Last updated: Feb 22 2024 at 05:02 UTC