def Lean.Options : Type

Equations

• Lean.Options = Lean.KVMap

Instances For

• Lean.instBEqOptions
• Lean.instForInOptionsProdNameDataValue
• Lean.instInhabitedOptions
• Lean.instToStringOptions

def Lean.Options.empty : Options

Equations

• Lean.Options.empty = { entries := [] }

instance Lean.instInhabitedOptions : Inhabited Options

Equations

• Lean.instInhabitedOptions = { default := { entries := [] } }

instance Lean.instToStringOptions : ToString Options

Equations

• Lean.instToStringOptions = inferInstanceAs (ToString Lean.KVMap)

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

Equations

• Lean.instForInOptionsProdNameDataValue = inferInstanceAs (ForIn m Lean.KVMap (Lean.Name × Lean.DataValue))

instance Lean.instBEqOptions : BEq Options

Equations

• Lean.instBEqOptions = inferInstanceAs (BEq Lean.KVMap)

structure Lean.OptionDecl : Type

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

Instances For

• Lean.instInhabitedOptionDecl

instance Lean.instInhabitedOptionDecl : Inhabited OptionDecl

Equations

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

def Lean.OptionDecls : Type

Equations

• Lean.OptionDecls = Lean.NameMap Lean.OptionDecl

Instances For

• Lean.instInhabitedOptionDecls

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

Instances

• Lean.Core.instMonadOptionsCoreM
• Lean.Elab.Command.instMonadOptionsCommandElabM
• Lean.Elab.Level.instMonadOptionsLevelElabM
• Lean.instMonadOptionsOfMonadLift

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 (Lean.KVMap.getBool opts 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 (Lean.KVMap.getNat opts k defValue)

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

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

Instances

• Lean.Core.instMonadWithOptionsCoreM
• Lean.instMonadWithOptionsOfMonadFunctor

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) => Lean.KVMap.setBool o `_inPattern true) x

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

Equations

• o.getInPattern = Lean.KVMap.getBool o `_inPattern

structure Lean.Option (α : Type) : Type

A strongly-typed reference to an option.

• name : Name
• defValue : α

Instances For

• Lean.instInhabitedOption

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

Equations

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

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

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.Option.set opts opt val = Lean.KVMap.set opts 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 Lean.KVMap.contains opts 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.