# 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.

def Lean.Elab.elabUnsetOption {m : } [inst : ] [inst : ] [inst : ] [inst : ] (id : Lean.Syntax) :

unset the option specified by id

Equations
• One or more equations did not get rendered due to their size.
def Lean.Elab.elabUnsetOption.unsetOption {m : } [inst : ] [inst : ] (optionName : Lean.Name) :

unset the given option name

Equations

Unset a user option

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