spaceloop (May 01 2021 at 14:12): 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.
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) .
spaceloop (May 02 2021 at 07:45):Thanks!
Last updated: Sep 25 2023 at 12:01 UTC