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

Equations

• Lean.Options.empty = { map := ∅, hasTrace := false }

instance Lean.Options.instInhabited : Inhabited Options

Equations

• Lean.Options.instInhabited = { default := Lean.Options.empty }

instance Lean.Options.instToString : ToString Options

Equations

• Lean.Options.instToString = { toString := fun (o : Lean.Options) => Lean.Options.instToString._private_1 o }

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

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Options.instBEq : BEq Options

Equations

• Lean.Options.instBEq = { beq := fun (o1 o2 : Lean.Options) => Lean.Options.instBEq._private_1 o1 o2 }

instance Lean.Options.instEmptyCollection : EmptyCollection Options

Equations

• Lean.Options.instEmptyCollection = { emptyCollection := Lean.Options.empty }

@[inline]

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

Equations

• o.find? k = (Lean.Options.map✝ o).find? k

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

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

Equations

• Lean.Options.find = Lean.Options.find?

@[inline]

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

Equations

• o.get? k = ((Lean.Options.map✝ o).find? k).bind Lean.KVMap.Value.ofDataValue?

@[inline]

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

Equations

• o.get k defVal = (o.get? k).getD defVal

@[inline]

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

Equations

• o.getBool k defVal = o.get k defVal

@[inline]

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

Equations

• o.contains k = (Lean.Options.map✝ o).contains k

@[inline]

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

Equations

• o.insert k v = { map := (Lean.Options.map✝ o).insert k v, hasTrace := o.hasTrace || `trace.isPrefixOf k }

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

Equations

• o.set k v = o.insert k (Lean.KVMap.Value.toDataValue v)

@[inline]

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

Equations

• o.setBool k v = o.set k v

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

Equations

• o.erase k = { map := Std.TreeMap.erase (Lean.Options.map✝ o) k, hasTrace := (Std.TreeMap.keys (Lean.Options.map✝¹ o)).any `trace.isPrefixOf }

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

Equations

• Lean.Options.mergeBy f o1 o2 = { map := Std.TreeMap.mergeWith f (Lean.Options.map✝ o1) (Lean.Options.map✝¹ o2), hasTrace := o1.hasTrace || o2.hasTrace }

structure Lean.OptionDecl : Type

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

instance Lean.instInhabitedOptionDecl : Inhabited OptionDecl

Equations

• Lean.instInhabitedOptionDecl = { default := Lean.instInhabitedOptionDecl.default }

def Lean.instInhabitedOptionDecl.default : OptionDecl

Equations

• Lean.instInhabitedOptionDecl.default = { name := default, declName := default, defValue := default, descr := default }

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

Equations

• One or more equations did not get rendered due to their size.

def Lean.OptionDecls : Type

Equations

• Lean.OptionDecls = Lean.NameMap Lean.OptionDecl

instance Lean.instInhabitedOptionDecls : Inhabited OptionDecls

Equations

• Lean.instInhabitedOptionDecls = { default := ∅ }

@[export lean_register_option]

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

Equations

• One or more equations did not get rendered due to their size.

def Lean.getOptionDecls : IO OptionDecls

Equations

• Lean.getOptionDecls = ST.Ref.get Lean.optionDeclsRef✝

@[export lean_get_option_decls_array]

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.getOptionDefaultValue name = do let decl ← Lean.getOptionDecl name pure decl.defValue

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

Equations

• Lean.getOptionDescr name = do let decl ← Lean.getOptionDecl name pure decl.descr

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

• getOptions : m Options

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

Equations

• Lean.instMonadOptionsOfMonadLift = { getOptions := liftM Lean.getOptions }

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

Equations

• Lean.getBoolOption k defValue = do let opts ← Lean.getOptions pure (opts.get k defValue)

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

Equations

• Lean.getNatOption k defValue = do let opts ← Lean.getOptions pure (opts.get k defValue)

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

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

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

Equations

• Lean.instMonadWithOptionsOfMonadFunctor = { withOptions := fun {α : Type} (f : Lean.Options → Lean.Options) (x : n α) => monadMap (fun {β : Type} => Lean.withOptions f) x }

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 α

Equations

• Lean.withInPattern x = Lean.withOptions (fun (o : Lean.Options) => o.set `_inPattern true) x

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

Equations

• o.getInPattern = o.get `_inPattern false

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✝

Equations

• Lean.instInhabitedOption.default = { name := default, defValue := default }

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

Equations

• Lean.instInhabitedOption = { default := Lean.instInhabitedOption.default }

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

• defValue : α
• descr : String

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

Equations

• Lean.Option.get? opts opt = opts.get? opt.name

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

Equations

• Lean.Option.get opts opt = opts.get opt.name opt.defValue

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

Equations

• opt.getM = do let __do_lift ← Lean.getOptions pure (Lean.Option.get __do_lift opt)

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

Equations

• Lean.Option.set opts opt val = opts.set opt.name val

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

Equations

• Lean.Option.setIfNotSet opts opt val = if opts.contains opt.name = true then opts else Lean.Option.set opts opt val

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

Equations

• One or more equations did not get rendered due to their size.

def Lean.Option.registerBuiltinOption : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Option.registerOption : ParserDescr

Equations

• One or more equations did not get rendered due to their size.