-
Notifications
You must be signed in to change notification settings - Fork 58
Consider adding Hint Mode for typeclasses #230
Copy link
Copy link
Open
Labels
enhancementNew feature or requestNew feature or request
Description
This project has many typeclass definition (100+ by a rough estimation). To lower the risk for library users of getting diverging type class resolution, consider adding explicit Hint Mode declarations for each typeclass or at least for key typeclasses. For example, the manual states:
Setting a parameter of a class as an input forces proof search to be driven by that index of the class
See the stdpp library base module for many examples of using Hint Mode.
Reactions are currently unavailable
Metadata
Metadata
Assignees
Labels
enhancementNew feature or requestNew feature or request