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

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

Instances For

• Lean.instBEqLOption
• Lean.instInhabitedLOption
• Lean.instToStringLOption

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} [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