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.

Equations

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

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.

Equations

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

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.

Equations

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

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

Strip optional suffixes from a binder name.

Equations

• Lean.Linter.List.stripBinderName s = ((((s.stripSuffix "'").stripSuffix "₁").stripSuffix "₂").stripSuffix "₃").stripSuffix "₄"

def Lean.Linter.List.allowedIndices : List String

Allowed names for index variables.

Equations

• Lean.Linter.List.allowedIndices = ["i", "j", "k", "start", "stop", "step"]

def Lean.Linter.List.allowedWidths : List String

Allowed names for width variables.

Equations

• Lean.Linter.List.allowedWidths = ["n", "m", "k", "l", "size"]

def Lean.Linter.List.allowedBitVecWidths : List String

Allowed names for BitVec width variables.

Equations

• Lean.Linter.List.allowedBitVecWidths = ["w"]

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.

Equations

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

def Lean.Linter.List.allowedListNames : List String

Allowed names for List variables.

Equations

• Lean.Linter.List.allowedListNames = ["l", "r", "s", "t", "tl", "ws", "xs", "ys", "zs", "as", "bs", "cs", "ds", "acc"]

def Lean.Linter.List.allowedArrayNames : List String

Allowed names for Array variables.

Equations

• Lean.Linter.List.allowedArrayNames = ["ws", "xs", "ys", "zs", "as", "bs", "cs", "ds", "acc"]

def Lean.Linter.List.allowedVectorNames : List String

Allowed names for Vector variables.

Equations

• Lean.Linter.List.allowedVectorNames = ["ws", "xs", "ys", "zs", "as", "bs", "cs", "ds", "acc"]

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.

Equations

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

def Lean.Linter.List.listVariablesLinter : Linter

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

Equations

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