Documentation

Lean.Linter.Basic

Linter sets are represented as a map from linter name to set name, to make it easy to look up which sets to check for enabling a linter.

Equations
    Instances For

      Insert a set into a LinterSets map.

      entry.1 is the name of the linter set, entry.2 contains the names of the set's linter options.

      Equations
        Instances For

          The LinterOptions structure is used to determine whether given linters are enabled.

          This structure contains all the data required to do so, the Options set on the command line or by the set_option command, and the LinterSets that have been declared.

          A single structure holding this data is useful since we want getLinterValue to be a pure function: determinining the LinterSets would otherwise require a MonadEnv instance.

          Instances For
            def Lean.Linter.LinterOptions.get {α : Type} [KVMap.Value α] (o : LinterOptions) (k : Name) (defVal : α) :
            α
            Equations
              Instances For
                Equations
                  Instances For
                    Equations
                      Instances For

                        Return the set of linter sets that this option is contained in.

                        Equations
                          Instances For
                            Equations
                              Instances For
                                Equations
                                  Instances For
                                    Equations
                                      Instances For
                                        def Lean.Linter.logLint {m : TypeType} [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] (linterOption : Lean.Option Bool) (stx : Syntax) (msg : MessageData) :
                                        Equations
                                          Instances For
                                            def Lean.Linter.logLintIf {m : TypeType} [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] [MonadEnv m] (linterOption : Lean.Option Bool) (stx : Syntax) (msg : MessageData) :

                                            If linterOption is enabled, print a linter warning message at the position determined by stx.

                                            Whether a linter option is enabled or not is determined by the following sequence:

                                            1. If it is set, then the value determines whether or not it is enabled.
                                            2. Otherwise, if linter.all is set, then its value determines whether or not the option is enabled.
                                            3. Otherwise, if any of the linter sets containing the option is enabled, it is enabled. (Only enabled linter sets are considered: explicitly disabling a linter set will revert the linters it contains to their default behavior.)
                                            4. Otherwise, the default value determines whether or not it is enabled.
                                            Equations
                                              Instances For