Documentation

Mathlib.Tactic.SudoSetOption

Defines the sudo set_option command. #

Allows setting undeclared options.

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.

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.