@[export lean_register_option]
Equations
Instances For
@[export lean_get_option_decls_array]
Equations
Instances For
Equations
def
Lean.getBoolOption
{m : Type → Type}
[Monad m]
[MonadOptions m]
(k : Name)
(defValue : Bool := false)
:
m Bool
Equations
Instances For
def
Lean.getNatOption
{m : Type → Type}
[Monad m]
[MonadOptions m]
(k : Name)
(defValue : Nat := 0)
:
m Nat
Equations
Instances For
instance
Lean.instMonadWithOptionsOfMonadFunctor
{m n : Type → Type}
[MonadFunctor m n]
[MonadWithOptions m]
:
Equations
Remark: _inPattern
is an internal option for communicating to the delaborator that
the term being delaborated should be treated as a pattern.
Equations
Instances For
Equations
Equations
Instances For
Equations
Instances For
Equations
Instances For
def
Lean.Option.setIfNotSet
{α : Type}
[KVMap.Value α]
(opts : Options)
(opt : Lean.Option α)
(val : α)
:
Similar to set
, but update opts
only if it doesn't already contains an setting for opt.name
Equations
Instances For
def
Lean.Option.register
{α : Type}
[KVMap.Value α]
(name : Name)
(decl : Option.Decl α)
(ref : Name := by exact decl_name%)
:
IO (Lean.Option α)