The haveI/letI linter

The tactics haveI and letI differ from have and let only in that they inline the given value into the term being constructed, instead of binding it with a have/let binder. (In Lean 3, haveI/letI were additionally needed to make the new hypothesis available to instance resolution; in Lean 4, have and let register local instances themselves, so inlining is the only remaining difference.)

Inside the proof of a proposition this difference is invisible: proofs are irrelevant, so nothing can depend on whether a value was inlined into the proof term. Hence haveI/letI are never needed in tactic proofs of propositions, and have/let should be used instead.

This linter flags every use of the haveI or letI tactic whose main goal is a proposition.

TODO:

• also lint the term-mode haveI/letI

opaque Mathlib.Linter.HaveILetI.linter.style.haveILetI : Lean.Option Bool

The haveILetI linter flags uses of the haveI or letI tactic in a proof of a proposition. Since proofs are irrelevant, the value-inlining behaviour of haveI/letI can have no effect there, and have/let should be used instead.

def Mathlib.Linter.HaveILetI.tacticHaveI__ : Lean.ParserDescr

haveI behaves like have, but inlines the value instead of producing a have term.

Equations

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

def Mathlib.Linter.HaveILetI.tacticLetI__ : Lean.ParserDescr

letI behaves like let, but inlines the value instead of producing a let term.

Equations

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