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.

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.

    Instances For