termSudoSet_option___In_ — Mathlib

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))
Похожие утверждения