Documentation

Lean.Data.LOption

source
inductive Lean.LOption (α : Type u) :
Type u
source
instance Lean.instInhabitedLOption:
{a : Type u_1} → Inhabited (Lean.LOption a)
Equations
  • Lean.instInhabitedLOption = { default := Lean.LOption.none }
source
instance Lean.instBEqLOption:
{α : Type u_1} → [inst : BEq α] → BEq (Lean.LOption α)
Equations
  • Lean.instBEqLOption = { beq := [anonymous] }
source
instance Lean.instToStringLOption {α : Type u_1} [inst : ToString α] :
ToString (Lean.LOption α)
Equations
  • One or more equations did not get rendered due to their size.
source
def Option.toLOption {α : Type u} :
Option α → Lean.LOption α
Equations
source
@[inline]
def toLOptionM {α : Type} {m : Type → Type} [inst : Monad m] (x : m (Option α)) :
m (Lean.LOption α)
Equations