Documentation

Batteries.Tactic.Lint.TypeClass

source
def Batteries.Tactic.Lint.impossibleInstance :
Linter

Lints for instances with arguments that cannot be filled in, like

instance {α β : Type} [Group α] : Mul α where ...
Instances For
    source
    def Batteries.Tactic.Lint.nonClassInstance :
    Linter

    A linter for checking if any declaration whose type is not a class is marked as an instance.

    Instances For