opaque Lean.Linter.linter.checkUnivs : Lean.Option Bool

Enables the checkUnivs linter, which warns when a declaration has a universe parameter that only ever occurs in a max u v together with another parameter, never on its own. This usually means that the type contains a max u v where neither u nor v occur by themselves; the fix is to provide the universe level explicitly.

def Lean.Linter.CheckUnivs.checkUnivsLinter : Linter

Enables the checkUnivs linter, which warns when a declaration has a universe parameter that only ever occurs in a max u v together with another parameter, never on its own. This usually means that the type contains a max u v where neither u nor v occur by themselves; the fix is to provide the universe level explicitly.

Equations

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