The have vs let linter

The have vs let linter flags uses of have to introduce a hypothesis whose Type is not Prop.

The option for this linter is a natural number, but really there are only 3 settings:

• 0 -- inactive;
• 1 -- active only on noisy declarations;
• 2 or more -- always active.

TODO:

• Also lint let vs have.
• haveI may need to change to let/letI?
• replace, classical!, classical, tauto internally use have: should the linter act on them as well?

opaque Mathlib.Linter.linter.haveLet : Lean.Option ℕ

The have vs let linter emits a warning on haves introducing a hypothesis whose Type is not Prop. There are three settings:

• 0 -- inactive;
• 1 -- active only on noisy declarations;
• 2 or more -- always active.

The default value is 1.

def Mathlib.Linter.haveLet.nonPropHaves : Lean.Elab.InfoTree → Lean.Elab.Command.CommandElabM (Array (Lean.Syntax × Std.Format))

returns the have syntax whose corresponding hypothesis does not have Type Prop and also a Formatted version of the corresponding Type.