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 Nat

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.isHave? : Lean.Syntax → Bool

find the have syntax.

def Mathlib.Linter.haveLet.InfoTree.foldInfoM {α : Type u_1} {m : Type u_1 → Type u_2} [Monad m] (f : Lean.Elab.ContextInfo → Lean.Elab.Info → α → m α) (init : α) : Lean.Elab.InfoTree → m α

a monadic version of Lean.Elab.InfoTree.foldInfo. Used to infer types inside a CommandElabM.

Equations

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

def Mathlib.Linter.haveLet.toFormat_propTypes (ctx : Lean.Elab.ContextInfo) (lc : Lean.LocalContext) (es : Array (Lean.Expr × Lean.Name)) : Lean.Elab.Command.CommandElabM (Array (Lean.Format × Lean.Name))

given a ContextInfo, a LocalContext and an Array of Expressions es with a Name, toFormat_propTypes creates a MetaM context, and returns an array of the pretty-printed Format of e, together with the (unchanged) name for each Expression e in es whose type is a Prop.

Concretely, toFormat_propTypes runs inferType in CommandElabM. This is the kind of monadic lift that nonPropHaves uses to decide whether the Type of a have is in Prop or not. The output Format is just so that the linter displays a better message.

Equations

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

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

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

Equations

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

def Mathlib.Linter.haveLet.haveLetLinter : Lean.Linter

The main implementation of the have vs let linter.

Equations

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