Documentation

Mathlib.Tactic.Linter.HaveLetLinter

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:

TODO:

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.

find the have syntax.

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

    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.
    Instances For

      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.
      Instances For

        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.
        Instances For

          The main implementation of the have vs let linter.

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