structure Lean.Options : Type

• map : Lean.NameMap Lean.DataValue
• hasTrace : Bool

  Whether any option with prefix trace is set. This does not imply that any of such option is set to true but it does capture the most common case that no such option has ever been touched.

def Lean.Options.empty : Options

@[instance_reducible]

instance Lean.Options.instInhabited : Inhabited Options

@[instance_reducible]

instance Lean.Options.instToString : ToString Options

@[instance_reducible]

instance Lean.Options.instForInProdNameDataValueOfMonad {m : Type u_1 → Type u_2} [Monad m] : ForIn m Options (Name × DataValue)

@[instance_reducible]

instance Lean.Options.instBEq : BEq Options

@[instance_reducible]

instance Lean.Options.instEmptyCollection : EmptyCollection Options

@[inline]

def Lean.Options.find? (o : Options) (k : Name) : Option DataValue

@[deprecated Lean.Options.find? (since := "2026-01-15")]

def Lean.Options.find (o : Options) (k : Name) : Option DataValue

@[inline]

def Lean.Options.get? {α : Type} [KVMap.Value α] (o : Options) (k : Name) : Option α

@[inline]

def Lean.Options.get {α : Type} [KVMap.Value α] (o : Options) (k : Name) (defVal : α) : α

@[inline]

def Lean.Options.getBool (o : Options) (k : Name) (defVal : Bool := false) : Bool

@[inline]

def Lean.Options.contains (o : Options) (k : Name) : Bool

@[inline]

def Lean.Options.insert (o : Options) (k : Name) (v : DataValue) : Options

def Lean.Options.set {α : Type} [KVMap.Value α] (o : Options) (k : Name) (v : α) : Options

@[inline]

def Lean.Options.setBool (o : Options) (k : Name) (v : Bool) : Options

def Lean.Options.erase (o : Options) (k : Name) : Options

def Lean.Options.mergeBy (f : Name → DataValue → DataValue → DataValue) (o1 o2 : Options) : Options

structure Lean.OptionDeprecation : Type

• since : String
• text? : Option String
• newName? : Option Name

  The option to use instead, taken from the @[deprecated <name>] attribute.

@[instance_reducible]

instance Lean.instInhabitedOptionDeprecation : Inhabited OptionDeprecation

structure Lean.OptionDecl : Type

• name : Name
• declName : Name
• defValue : DataValue
• descr : String
• deprecation? : Option OptionDeprecation

@[instance_reducible]

instance Lean.instInhabitedOptionDecl : Inhabited OptionDecl

def Lean.OptionDecl.fullDescr (self : OptionDecl) : String

def Lean.OptionDecls : Type

@[instance_reducible]

instance Lean.instInhabitedOptionDecls : Inhabited OptionDecls

@[export lean_register_option]

def Lean.registerOption (name : Name) (decl : OptionDecl) : IO Unit

def Lean.getOptionDecls : IO OptionDecls

def Lean.getOptionDecl (name : Name) : IO OptionDecl

def Lean.getOptionDefaultValue (name : Name) : IO DataValue

def Lean.getOptionDescr (name : Name) : IO String

class Lean.MonadOptions (m : Type → Type) : Type

• getOptions : m Options
• getOptionsUnrestricted : m Options

  Returns the options without the check of getOptions for recording computations. Only for reads that cannot influence a result cached by such a computation: message rendering, trace and profiler collection, diagnostics, and limits that are part of the cache key or throw when exceeded. See Lean.getRecordedOption.

@[instance_reducible]

instance Lean.instMonadOptionsOfMonadLift {m n : Type → Type} [MonadLift m n] [MonadOptions m] : MonadOptions n

def Lean.getBoolOption {m : Type → Type} [Monad m] [MonadOptions m] (k : Name) (defValue : Bool := false) : m Bool

def Lean.getNatOption {m : Type → Type} [Monad m] [MonadOptions m] (k : Name) (defValue : Nat := 0) : m Nat

class Lean.MonadWithOptions (m : Type → Type) : Type 1

• withOptions {α : Type} (f : Options → Options) (x : m α) : m α

@[instance_reducible]

instance Lean.instMonadWithOptionsOfMonadFunctor {m n : Type → Type} [MonadFunctor m n] [MonadWithOptions m] : MonadWithOptions n

Remark: _inPattern is an internal option for communicating to the delaborator that the term being delaborated should be treated as a pattern.

def Lean.withInPattern {m : Type → Type} {α : Type} [MonadWithOptions m] (x : m α) : m α

def Lean.Options.getInPattern (o : Options) : Bool

structure Lean.Option (α : Type) : Type

A strongly-typed reference to an option.

• name : Name
• defValue : α

@[instance_reducible]

instance Lean.instInhabitedOption {a✝ : Type} [Inhabited a✝] : Inhabited (Lean.Option a✝)

structure Lean.Option.Decl (α : Type) : Type

• defValue : α
• descr : String
• deprecation? : Option OptionDeprecation

def Lean.Option.get? {α : Type} [KVMap.Value α] (opts : Options) (opt : Lean.Option α) : Option α

def Lean.Option.get {α : Type} [KVMap.Value α] (opts : Options) (opt : Lean.Option α) : α

def Lean.Option.getM {m : Type → Type} {α : Type} [Monad m] [MonadOptions m] [KVMap.Value α] (opt : Lean.Option α) : m α

def Lean.Option.set {α : Type} [KVMap.Value α] (opts : Options) (opt : Lean.Option α) (val : α) : Options

def Lean.Option.setIfNotSet {α : Type} [KVMap.Value α] (opts : Options) (opt : Lean.Option α) (val : α) : Options

Similar to set, but update opts only if it doesn't already contains an setting for opt.name

def Lean.Option.register {α : Type} [KVMap.Value α] (name : Name) (decl : Option.Decl α) (ref : Name := by exact decl_name%) : IO (Lean.Option α)

def Lean.Option.registerBuiltinOption : ParserDescr

def Lean.Option.registerOption : ParserDescr