Stream: Coq devs & plugin devs

Topic: Program mode and typeclasses


view this post on Zulip Jason Gross (Nov 24 2022 at 20:19):

Why does Program fail if there are implicit typeclasses holes that cannot be resolved? Is there a way to make Program turn them into obligations instead?

view this post on Zulip Paolo Giarrusso (Nov 24 2022 at 20:36):

https://github.com/coq/coq/issues/12147 seems relevant and has a workaround

Definition disable_tc {T : Type} (x : id T) : T := x.
Notation notc_hole := (disable_tc _).

even if that _will_ be annoying for implicit arguments

view this post on Zulip Jason Gross (Nov 24 2022 at 21:10):

This doesn't help when I can't figure out where the typeclass hole is in the first place, unfortunately, and I want obligations to help me figure out where they are. (I can stuff the type and code in refine in a Goal, but that doesn't work as well when the code is relying on the casts that Program inserts...)


Last updated: Feb 05 2023 at 22:03 UTC