Linters for Mathlib

In this file we define additional linters for mathlib.

Perhaps these should be moved to Std in the future.

def Std.Tactic.Lint.structureInType : Std.Tactic.Lint.Linter

Linter that checks whether a structure should be in Prop.

Equations

• One or more equations did not get rendered due to their size.