Stream: Coq users

Topic: Encoding `Unifall` via boilerplate-generating plugins

view this post on Zulip 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: Jun 20 2024 at 11:02 UTC