Stream: Coq users

Topic: ✔ Retroactively add Typeclasses Unique Instances


view this post on Zulip Thibaut Pérami (Mar 14 2024 at 15:12):

No, that won't really work for me because most instance of A that I use are also defined in the library and use A itself, so I would have to just redo everything. I think might have to fork the library locally then

view this post on Zulip Ike Mulder (Mar 14 2024 at 15:14):

Perhaps you could wrap the required instances in stdpp's TCNoBackTrack?

view this post on Zulip Thibaut Pérami (Mar 14 2024 at 15:21):

Yes, but I don't control when A is called, e.g. MBind. If I use the _ ← _; _ notation of stdpp, then it will do a backtracking search over MBind even if I didn't want it to, and there is no easy way to change that, even with TCNoBackTrack

view this post on Zulip Thibaut Pérami (Mar 14 2024 at 15:24):

Also, TCNoBackTrack only works on type classes in Prop, not in Type

view this post on Zulip Thibaut Pérami (Mar 14 2024 at 15:47):

But actually, I now realize (after trying with a copied typeclass) that this flag is not really doing what I want anyway, don't bother with this

view this post on Zulip Notification Bot (Mar 14 2024 at 15:47):

Thibaut Pérami has marked this topic as resolved.


Last updated: Jun 23 2024 at 05:02 UTC