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.

source
def Lean.Elab.elabUnsetOption {m : Type → Type} [Monad m] [Lean.MonadOptions m] [Lean.MonadRef m] [Lean.Elab.MonadInfoTree m] (id : Lean.Syntax) :
m Lean.Options

unset the option specified by id

Instances For
    source
    def Lean.Elab.elabUnsetOption.unsetOption {m : Type → Type} [Monad m] [Lean.MonadOptions m] (optionName : Lean.Name) :
    m Lean.Options

    unset the given option name

    Instances For
      source
      def Lean.Elab.Command.unsetOption :
      Lean.ParserDescr

      Unset a user option

      Instances For