def Lean.Options : Type

def Lean.Options.empty : Lean.Options

instance Lean.instInhabitedOptions : Inhabited Lean.Options

instance Lean.instToStringOptions : ToString Lean.Options

instance Lean.instForInOptionsProdNameDataValue {m : Type u_1 → Type u_2} : ForIn m Lean.Options (Lake.Name × Lean.DataValue)

instance Lean.instBEqOptions : BEq Lean.Options

structure Lean.OptionDecl : Type

• declName : Lake.Name
• defValue : Lean.DataValue
• group : String
• descr : String

instance Lean.instInhabitedOptionDecl : Inhabited Lean.OptionDecl

def Lean.OptionDecls : Type

instance Lean.instInhabitedOptionDecls : Inhabited Lean.OptionDecls

@[export lean_register_option]

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

def Lean.getOptionDecls : IO Lean.OptionDecls

@[export lean_get_option_decls_array]

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

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

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

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

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

• getOptions : m Lean.Options

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

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

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

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

• withOptions : {α : Type} → (Lean.Options → Lean.Options) → m α → m α

instance Lean.instMonadWithOptions {m : Type → Type} {n : Type → Type} [MonadFunctor m n] [Lean.MonadWithOptions m] : Lean.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} [Lean.MonadWithOptions m] (x : m α) : m α

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

structure Lean.Option (α : Type) : Type

• name : Lake.Name
• defValue : α

A strongly-typed reference to an option.

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

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

• defValue : α
• group : String
• descr : String

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

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

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

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

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

def Lean.Option.register {α : Type} [Lean.KVMap.Value α] (name : Lake.Name) (decl : Lean.Option.Decl α) (ref : autoParam Lake.Name _auto✝) : IO (Lean.Option α)

def Lean.Option.registerBuiltinOption : Lean.ParserDescr

def Lean.Option.registerOption : Lean.ParserDescr