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

Enables the defProp linter, which warns when a def is used to introduce a declaration whose type is a Prop. Such a declaration should be written using theorem instead.

def Lean.Linter.DefProp.defPropLinter : Linter

Enables the defProp linter, which warns when a def is used to introduce a declaration whose type is a Prop. Such a declaration should be written using theorem instead.

Equations

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