DeepSpec / InteractionTrees

A Library for Representing Recursive and Impure Programs in Coq
MIT License
194 stars 49 forks source link

Consider adding Hint Mode for typeclasses #230

Open palmskog opened 2 years ago

palmskog commented 2 years ago

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.