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