Lean.Data.Options

source

def Lean.Options:

Type

Equations

Lean.Options = Lean.KVMap

source

def Lean.Options.empty:

Lean.Options

Equations

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

source

instance Lean.instInhabitedOptions:

Inhabited Lean.Options

Equations

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

source

instance Lean.instToStringOptions:

ToString Lean.Options

Equations

Lean.instToStringOptions = inferInstanceAs (ToString Lean.KVMap)

source

instance Lean.instForInOptionsProdNameDataValue {m : Type u_1 → Type u_2} :

ForIn m Lean.Options (Lean.Name × Lean.DataValue)

Equations

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

source

structure Lean.OptionDecl:

Type

defValue : Lean.DataValue
group : String
descr : String

source

instance Lean.instInhabitedOptionDecl:

Inhabited Lean.OptionDecl

Equations

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

source

def Lean.OptionDecls:

Type

Equations

Lean.OptionDecls = Lean.NameMap Lean.OptionDecl

source

instance Lean.instInhabitedOptionDecls:

Inhabited Lean.OptionDecls

Equations

Lean.instInhabitedOptionDecls = { default := ∅ }

source

@[export lean_register_option]

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

IO Unit

Equations

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

source

def Lean.getOptionDecls:

IO Lean.OptionDecls

Equations

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

source

@[export lean_get_option_decls_array]

def Lean.getOptionDeclsArray:

IO (Array (Lean.Name × Lean.OptionDecl))

Equations

Lean.getOptionDeclsArray = do let decls ← Lean.getOptionDecls pure (Std.RBMap.fold (fun r k v => Array.push r (k, v)) #[] decls)

source

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

IO Lean.OptionDecl

Equations

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

source

def Lean.getOptionDefaulValue (name : Lean.Name) :

IO Lean.DataValue

Equations

Lean.getOptionDefaulValue name = do let decl ← Lean.getOptionDecl name pure decl.defValue

source

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

IO String

Equations

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

source

def Lean.setOptionFromString (opts : Lean.Options) (entry : String) :

IO Lean.Options

Equations

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

source

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

Type

getOptions : m Lean.Options

Instances

source

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

Lean.MonadOptions n

Equations

Lean.instMonadOptions = { getOptions := liftM Lean.getOptions }

source

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

m Bool

Equations

Lean.getBoolOption k defValue = do let opts ← Lean.getOptions pure (Lean.KVMap.getBool opts k defValue)

source

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

m Nat

Equations

Lean.getNatOption k defValue = do let opts ← Lean.getOptions pure (Lean.KVMap.getNat opts k defValue)

source

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

Type 1

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

Instances

source

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

Lean.MonadWithOptions n

Equations

Lean.instMonadWithOptions = { withOptions := fun {α} f x => monadMap (fun {β} => Lean.withOptions f) x }

source

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

m α

Equations

Lean.withInPattern x = Lean.withOptions (fun o => Lean.KVMap.setBool o `_inPattern true) x

source

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

Bool

Equations

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

source

structure Lean.Option (α : Type) :

Type

name : Lean.Name
defValue : α

A strongly-typed reference to an option.

source

instance Lean.instInhabitedOption:

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

Equations

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

source

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

Type

defValue : α
group : String
descr : String

source

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

Option α

Equations

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

source

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

Equations

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

source

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

Lean.Options

Equations

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

source

def Lean.Option.setIfNotSet {α : Type} [inst : 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

Equations

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

source

def Lean.Option.register {α : Type} [inst : Lean.KVMap.Value α] (name : Lean.Name) (decl : Lean.Option.Decl α) :

IO (Lean.Option α)

Equations

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

source

def Lean.Option.«commandRegister_builtin_option_:_:=_»:

Lean.ParserDescr

Equations

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

source

def Lean.Option.«commandRegister_option_:_:=_»:

Lean.ParserDescr

Equations

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