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

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

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

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

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

Equations

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

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