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

@[implicit_reducible]

instance Lean.Options.instInhabited : Inhabited Options

@[implicit_reducible]

instance Lean.Options.instToString : ToString Options

@[implicit_reducible]

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

@[implicit_reducible]

instance Lean.Options.instBEq : BEq Options

@[implicit_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.OptionDecl : Type

• name : Name
• declName : Name
• defValue : DataValue
• descr : String

@[implicit_reducible]

instance Lean.instInhabitedOptionDecl : Inhabited OptionDecl

def Lean.instInhabitedOptionDecl.default : OptionDecl

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

def Lean.OptionDecls : Type

@[implicit_reducible]

instance Lean.instInhabitedOptionDecls : Inhabited OptionDecls

@[export lean_register_option]

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

def Lean.getOptionDecls : IO OptionDecls

@[export lean_get_option_decls_array]

def Lean.getOptionDeclsArray : IO (Array (Name × OptionDecl))

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

@[implicit_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 α

@[implicit_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 : α

def Lean.instInhabitedOption.default {a✝ : Type} [Inhabited a✝] : Lean.Option a✝

@[implicit_reducible]

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

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

• defValue : α
• descr : String

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