Skip to content

Consider adding Hint Mode for typeclasses #230

@palmskog

Description

@palmskog

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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    enhancementNew feature or request

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions