inductive Lean.LOption (α : Type u) : Type u

• none {α : Type u} : LOption α
• some {α : Type u} : α → LOption α
• undef {α : Type u} : LOption α

instance Lean.instInhabitedLOption {a✝ : Type u_1} : Inhabited (LOption a✝)

Equations

• Lean.instInhabitedLOption = { default := Lean.LOption.none }

instance Lean.instBEqLOption {α✝ : Type u_1} [BEq α✝] : BEq (LOption α✝)

Equations

• Lean.instBEqLOption = { beq := Lean.beqLOption✝ }

instance Lean.instToStringLOption {α : Type u_1} [ToString α] : ToString (LOption α)

Equations

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

def Lean.LOption.toOption {α : Type u_1} : LOption α → Option α

Equations

• (Lean.LOption.some a).toOption = some a
• x✝.toOption = none

def Option.toLOption {α : Type u} : Option α → Lean.LOption α

Equations

• none.toLOption = Lean.LOption.none
• (some a).toLOption = Lean.LOption.some a

@[inline]

def toLOptionM {α : Type} {m : Type → Type} [Monad m] (x : m (Option α)) : m (Lean.LOption α)

Equations

• toLOptionM x = do let b ← x pure b.toLOption