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)

partial def Lean.withSetOptionIn (cmd : Elab.Command.CommandElab) : Elab.Command.CommandElab

Given a command elaborator cmd, returns a new command elaborator that first peels off and evaluates set_option ... in ... syntax recursively, updating the options accordingly, and then invokes cmd on the inner syntax.

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.