Yannick Forster (Oct 16 2020 at 14:29): Yannick Forster (Oct 16 2020 at 14:29):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?
Matthieu Sozeau (Oct 16 2020 at 16:36):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 :)
Maxime Dénès (Oct 16 2020 at 16:38):I thought we agreed that auto with * was a disaster
Maxime Dénès (Oct 16 2020 at 16:39):but I guess you could instead have a dictionary of equations
Matthieu Sozeau (Oct 16 2020 at 17:34):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)
Paolo Giarrusso (Oct 16 2020 at 18:15):Does Ltac2 have first-class databases?
Paolo Giarrusso (Oct 16 2020 at 18:17):it would be nice to have APIs to get lists of hint databases, and then access their properties.
Paolo Giarrusso (Oct 16 2020 at 18:17):oh, and possibly iterate over hints.
Paolo Giarrusso (Oct 16 2020 at 18:18):would this require rewriting the underlying internals? plugins to iterate over hints exist, so it’s at least not impossible in OCaml
Matthieu Sozeau (Oct 16 2020 at 21:39):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: Apr 20 2024 at 02:40 UTC