Paolo Giarrusso (Jul 07 2020 at 08:54): Paolo Giarrusso (Jul 07 2020 at 08:54):When tactic unification fails to apply a typeclass instance, one can replace the instance by a Lemma + a Hint Extern using apply:. That happens sometimes in Iris, for instance.
Stupid question: Could this pattern be encapsulated in a plugin, providing some Unifall_Instance command? Or are the resulting instances too slow?
Last updated: Oct 05 2023 at 02:01 UTC