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.