Defines the sudo set_option command.

Allows setting undeclared options.

def commandSudoSet_option___ : Lean.ParserDescr

The command sudo set_option name val is similar to set_option name val, but it also allows to set undeclared options.

def termSudoSet_option___In_ : Lean.ParserDescr

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.