Stream: MetaCoq

Topic: Recursive Quote Tactic

view this post on Zulip Pierre Vial (Mar 04 2021 at 10:43):

Hi,
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 MetaCoq?

view this post on Zulip Yannick Forster (Mar 04 2021 at 10:44):

Instead of quote_term you should be able to use the run_template_program tactic and then use tmQuoteRec

view this post on Zulip Pierre Vial (Mar 04 2021 at 10:50):

OK, thanks one more time Yannick :)

Last updated: Apr 18 2024 at 07:02 UTC