Documentation

Lean.Data.Options

Equations
Instances For
Equations
@[export lean_register_option]
Equations
  • One or more equations did not get rendered due to their size.
@[export lean_get_option_decls_array]
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
Equations
  • Lean.instMonadOptionsOfMonadLift = { getOptions := liftM Lean.getOptions }
def Lean.getBoolOption {m : TypeType} [Monad m] [Lean.MonadOptions m] (k : Lake.Name) (defValue : optParam Bool false) :
Equations
def Lean.getNatOption {m : TypeType} [Monad m] [Lean.MonadOptions m] (k : Lake.Name) (defValue : optParam Nat 0) :
m Nat
Equations
Equations

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 : TypeType} {α : Type} [Lean.MonadWithOptions m] (x : m α) :
m α
Equations
Equations
structure Lean.Option (α : Type) :

A strongly-typed reference to an option.

Instances For
instance Lean.instInhabitedOption :
{a : Type} → [inst : Inhabited a] → Inhabited (Lean.Option a)
Equations
  • Lean.instInhabitedOption = { default := { name := default, defValue := default } }
structure Lean.Option.Decl (α : Type) :
def Lean.Option.get? {α : Type} [Lean.KVMap.Value α] (opts : Lean.Options) (opt : Lean.Option α) :
Equations
def Lean.Option.get {α : Type} [Lean.KVMap.Value α] (opts : Lean.Options) (opt : Lean.Option α) :
α
Equations
def Lean.Option.set {α : Type} [Lean.KVMap.Value α] (opts : Lean.Options) (opt : Lean.Option α) (val : α) :
Equations
def Lean.Option.setIfNotSet {α : Type} [Lean.KVMap.Value α] (opts : Lean.Options) (opt : Lean.Option α) (val : α) :

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

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