This file defines style linters for the List/Array/Vector modules.

Currently, we do not anticipate that they will be useful elsewhere.

opaque Lean.Linter.List.linter.indexVariables : Lean.Option Bool

set_option linter.indexVariables true enables a strict linter that validates that the only variables appearing as an index (e.g. in xs[i] or xs.take i) are i, j, or k, and similarly that the only variables appearing as a width (e.g. in List.replicate n a or Vector α n) are n or m.

opaque Lean.Linter.List.linter.listVariables : Lean.Option Bool

set_option linter.listVariables true enables a strict linter that validates that all List/Array/Vector variables use standardized names.

def Lean.Linter.List.numericalIndices (t : Elab.InfoTree) : List (Syntax × Name)

Return the syntax for all expressions in which an fvarId appears as a "numerical index", along with the user name of that fvarId.

def Lean.Linter.List.numericalWidths (t : Elab.InfoTree) : List (Syntax × Name)

Return the syntax for all expressions in which an fvarId appears as a "numerical width", along with the user name of that fvarId.

def Lean.Linter.List.bitVecWidths (t : Elab.InfoTree) : List (Syntax × Name)

Return the syntax for all expressions in which an fvarId appears as a "BitVec width", along with the user name of that fvarId.

def Lean.Linter.List.stripBinderName (s : String) : String

Strip optional suffixes from a binder name.

def Lean.Linter.List.allowedIndices : List String

Allowed names for index variables.

def Lean.Linter.List.allowedWidths : List String

Allowed names for width variables.

def Lean.Linter.List.allowedBitVecWidths : List String

Allowed names for BitVec width variables.

def Lean.Linter.List.indexLinter : Linter

A linter which validates that the only variables used as "indices" (e.g. in xs[i] or xs.take i) are i, j, or k.

def Lean.Linter.List.allowedListNames : List String

Allowed names for List variables.

def Lean.Linter.List.allowedArrayNames : List String

Allowed names for Array variables.

def Lean.Linter.List.allowedVectorNames : List String

Allowed names for Vector variables.

def Lean.Linter.List.binders (t : Elab.InfoTree) (p : Expr → Bool := fun (x : Expr) => true) : IO (List (Syntax × Name × Expr))

Find all binders appearing in the given info tree.

def Lean.Linter.List.listVariablesLinter : Linter

A linter which validates that all List/Array/Vector variables use allowed names.