feat: set_option for conv mode

[lecopivo]

Setting options with set_option ... in ... was only possible in tactic mode. This PR enables it to do it in conv mode too.

The only issue with my fix is that the syntax definition is in src/Lean/Elab/Tactic/Conv/Basic.lean which is clearly a bad place for it. Ideally it should be in src/Lean/Parser/Command.lean just next to the definition of set_option tactic but I do not know how to write the parser with convSeq

[digama0]

You need

  register_parser_alias                                                 optionValue

around here and then (after a stage0 update)

syntax (name := «set_option») "set_option " ident ppSpace optionValue " in " convSeq : conv

in Init/Conv.lean to define the syntax here.

You can probably also implement the conv as a macro, not just define the syntax, by transitioning in and out of tactic mode, c.f. the focus conv tactic.

[leanprover-community-mathlib4-bot]

• ❗ Mathlib CI will not be attempted unless you rebase your PR onto the 'nightly' branch. (2023-11-15 20:48:42)