The unset_option command #
This file defines an unset_option user command, which unsets user configurable
options.
For example, inputting 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 : Type → Type}
[Monad m]
[MonadOptions m]
[MonadRef m]
[MonadInfoTree m]
(id : Syntax)
:
m Options
unset the option specified by id
Equations
Instances For
def
Lean.Elab.elabUnsetOption.unsetOption
{m : Type → Type}
[Monad m]
[MonadOptions m]
(optionName : Name)
:
m Options
unset the given option name