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

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

def Lean.instInhabitedLOption.default {a✝ : Type u_1} : LOption a✝

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

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

def Lean.instBEqLOption.beq {α✝ : Type u_1} [BEq α✝] : LOption α✝ → LOption α✝ → Bool

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

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

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

@[inline]

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