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 : Type → Type}
[inst : Monad m]
[inst : Lean.MonadOptions m]
[inst : Lean.MonadRef m]
[inst : Lean.Elab.MonadInfoTree m]
(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 : Type → Type}
[inst : Monad m]
[inst : Lean.MonadOptions m]
(optionName : Lean.Name)
:
unset the given option name
Equations
- Lean.Elab.elabUnsetOption.unsetOption optionName = do let __do_lift ← Lean.getOptions pure (Lean.KVMap.erase __do_lift optionName)
Unset a user option
Equations
- One or more equations did not get rendered due to their size.