Documentation

Lean.Data.LOption

source
inductive Lean.LOption (α : Type u) :
Type u
source
instance Lean.instInhabitedLOption :
{a : Type u_1} → Inhabited (Lean.LOption a)
Equations
  • Lean.instInhabitedLOption = { default := Lean.LOption.none }
source
instance Lean.instBEqLOption :
{α : Type u_1} → [inst : BEq α] → BEq (Lean.LOption α)
Equations
  • Lean.instBEqLOption = { beq := [anonymous] }
source
instance Lean.instToStringLOption {α : Type u_1} [inst : ToString α] :
ToString (Lean.LOption α)
Equations
  • Lean.instToStringLOption = { toString := fun x => match x with | Lean.LOption.none => "none" | Lean.LOption.undef => "undef" | Lean.LOption.some a => "(some " ++ toString a ++ ")" }
source
def Option.toLOption {α : Type u} :
Option α → Lean.LOption α
Equations
source
@[inline]
def toLOptionM {α : Type} {m : Type → Type} [inst : Monad m] (x : m (Option α)) :
m (Lean.LOption α)
Equations