Stream: Coq users

Topic: Implementing destruct-like tactic


view this post on Zulip spaceloop (May 01 2021 at 14:12):

Is it possible to implement a tactic that can inspect the structure of an inductive type? I'd like to generically generate some match patterns, similar to what destruct/inversion etc are capable of.

view this post on Zulip Kenji Maillard (May 01 2021 at 14:37):

You can do that in Ltac2 for sure (using the Ltac2.Ind module). Slightly more heavy solutions would leverage Elpi (examples in this paper) or Metacoq (as a reification plugin; see here). You can also abuse Ltac hacks (see for instance the coq deriving library) .

view this post on Zulip spaceloop (May 02 2021 at 07:45):

Thanks!


Last updated: Jan 31 2023 at 13:02 UTC