Defines the sudo set_option command.

Allows setting undeclared options.

ink

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.

Equations

• One or more equations did not get rendered due to their size.

ink

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.

Equations

• One or more equations did not get rendered due to their size.