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.
Instances For

    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.
    Instances For