Hi all, I want to do call the simp
tactic from the Equations plugin to simplify all possible occurrences of a function defined using Equations in the goal. Is it possible, or do I have to pass the names of all functions manually?
Currently the simp
tactic is just an alias to autorewrite
and it's not possible to give "all" databases to it (like auto with *), but that's surely a good feature request :)
I thought we agreed that auto with *
was a disaster
but I guess you could instead have a dictionary of equations
Yes, you don't want a with *
, but rather a way to refer to all the equations
(and maybe even have more fine grained set-like operations on databases)
Does Ltac2 have first-class databases?
it would be nice to have APIs to get lists of hint databases, and then access their properties.
oh, and possibly iterate over hints.
would this require rewriting the underlying internals? plugins to iterate over hints exist, so it’s at least not impossible in OCaml
I think the main issue if any is to persist this state indeed, which should ideally just be a set of global names. I guess Ltac2 would fit here indeed. @Pierre-Marie Pédrot ?
Last updated: Oct 13 2024 at 01:02 UTC