Documentation

Lean.Linter.Basic

Basic linting functionality #

This file publicly imports the basic functionality necessary for linting, namely

  1. The linter option API (Lean.Linter.Init)
  2. The CommandElabM API (Lean.Elab.Command)
source
partial def Lean.withSetOptionIn {α : Type} (cmd : Syntax → Elab.Command.CommandElabM α) :
Syntax → Elab.Command.CommandElabM α

Given a function cmd on command syntax, returns a new function that first peels off and evaluates set_option ... in ... syntax recursively, updating the options accordingly, and then invokes cmd on the inner syntax. The result type is arbitrary, so that besides CommandElabs this can also wrap functions that return values, such as the phases of a stateful linter.

This is expected to be used in linters, after elaboration is complete. It is not appropriate for ordinary elaboration of outer set_options, since it

  • does not update the infotrees with info for the set_option commands
  • silently ignores failures in setting the given options (e.g. we do not error if the option is unknown or the wrong type of value is provided), as these should have been reported during original elaboration.