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: Jan 28 2023 at 06:30 UTC