Lints for instances with arguments that cannot be filled in, like
instance {α β : Type} [Group α] : Mul α where ...
Equations
Instances For
A linter for checking if any declaration whose type is not a class is marked as an instance.
Lints for instances with arguments that cannot be filled in, like
instance {α β : Type} [Group α] : Mul α where ...
A linter for checking if any declaration whose type is not a class is marked as an instance.