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))