commandSudoSet_option___ — Mathlib

Lean4

/-- The command `sudo set_option name val` is similar to `set_option name val`,
but it also allows to set undeclared options.
-/
@[command_parser 1000]
public meta def commandSudoSet_option___ : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `commandSudoSet_option___ 1022
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen
          (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "sudo ") (ParserDescr.symbol✝ "set_option "))
          (ParserDescr.const✝ `ident))
        (ParserDescr.unary✝ `group (ParserDescr.const✝ `ppSpace)))
      (ParserDescr.cat✝ `term 0))

Похожие утверждения