source
def Lean.Options :
Type
Equations

- Lean.Options = Lean.KVMap

Instances For

source
def Lean.Options.empty :
Options
Equations

- Lean.Options.empty = { }

Instances For

source
instance Lean.instInhabitedOptions :
Inhabited Options
Equations

- Lean.instInhabitedOptions = { default := { } }

source
instance Lean.instToStringOptions :
ToString Options
Equations

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

source
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))

source
instance Lean.instBEqOptions :
BEq Options
Equations

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

source
structure Lean.OptionDecl :
Type

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

Instances For

source
def Lean.instInhabitedOptionDecl.default :
OptionDecl
Equations

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

Instances For

source
instance Lean.instInhabitedOptionDecl :
Inhabited OptionDecl
Equations

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

source
def Lean.OptionDecls :
Type
Equations

- Lean.OptionDecls = Lean.NameMap Lean.OptionDecl

Instances For

source
instance Lean.instInhabitedOptionDecls :
Inhabited OptionDecls
Equations

- Lean.instInhabitedOptionDecls = { default := ∅ }

source
@[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.

Instances For

source
def Lean.getOptionDecls :
IO OptionDecls
Equations

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

Instances For

source
@[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.

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

- getOptions : m Options

Instances

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

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

source
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)

Instances For

source
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)

Instances For

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

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

Instances

source
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.

source
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

Instances For

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

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

Instances For

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

A strongly-typed reference to an option.

- name : Name
- defValue : α

Instances For

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

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

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

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

Instances For

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

- defValue : α
- group : String
- descr : String

Instances For

source
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

Instances For

source
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

Instances For

source
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)

Instances For

source
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

Instances For

source
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

Instances For

source
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.

Instances For

source
def Lean.Option.registerBuiltinOption :
ParserDescr
Equations

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

Instances For

source
def Lean.Option.registerOption :
ParserDescr
Equations

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

Instances For