Documentation

Lean.Linter.List

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

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

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.

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

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

Equations
    Instances For

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

      Equations
        Instances For

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

          Equations
            Instances For

              Strip optional suffixes from a binder name.

              Equations
                Instances For

                  Allowed names for index variables.

                  Equations
                    Instances For

                      Allowed names for width variables.

                      Equations
                        Instances For

                          Allowed names for BitVec width variables.

                          Equations
                            Instances For

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

                                  Allowed names for List variables.

                                  Equations
                                    Instances For

                                      Allowed names for Array variables.

                                      Equations
                                        Instances For

                                          Allowed names for Vector variables.

                                          Equations
                                            Instances For
                                              def Lean.Linter.List.binders (t : Elab.InfoTree) (p : ExprBool := fun (x : Expr) => true) :

                                              Find all binders appearing in the given info tree.

                                              Equations
                                                Instances For

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

                                                  Equations
                                                    Instances For