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.areProp_toFormat (ctx : Lean.Elab.ContextInfo) (lc : Lean.LocalContext) (es : Array Lean.Expr) : Lean.Elab.Command.CommandElabM (Array (Bool × Lean.Format))

given a ContextInfo, a LocalContext and an Array of Expressions es, areProp_toFormat creates a MetaM context, and returns an array of pairs consisting of

• a Boolean, answering the question of whether the Type of e is a Prop or not, and
• the pretty-printed Format of e for each Expression e in es. Concretely, areProp_toFormat 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.