Lean4
/-- The command `sudo set_option name val in term` is similar to `set_option name val in term`,
but it also allows to set undeclared options.
-/
@[term_parser 1000]
public meta def termSudoSet_option___In_ : Lean.ParserDescr✝ :=
ParserDescr.node✝ `termSudoSet_option___In_ 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(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))
(ParserDescr.symbol✝ " in "))
(ParserDescr.cat✝ `term 0))