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)

Equations

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

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

Equations

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

instance Lean.instToStringLOption {α : Type u_1} [inst : 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

• Option.toLOption x = match x with | none => Lean.LOption.none | some a => Lean.LOption.some a

@[inline]

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

Equations

• toLOptionM x = do let b ← x pure (Option.toLOption b)