Documentation

Mathlib.Tactic.UnsetOption

The unset_option command #

This file defines an unset_option user command, which unsets user configurable options. For example inputing set_option blah 7 and then unset_option blah returns the user to the default state before any set_option command is called. This is helpful when the user does not know the default value of the option or it is cleaner not to write it explicitly, or for some options where the default behaviour is different from any user set value.

unset the option specified by id

Instances For

    unset the given option name

    Instances For

      Unset a user option

      Instances For