Documentation

Init.Data.Option.Basic

def Option.toMonad {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] [inst : Alternative m] :

Option α → m α

Equations

Option.toMonad _fun_discr = match _fun_discr with | none => failure | some a => pure a

@[inline]

def Option.toBool {α : Type u_1} :

Option α → Bool

Equations

Option.toBool _fun_discr = match _fun_discr with | some val => true | none => false

@[inline]

def Option.isSome {α : Type u_1} :

Option α → Bool

Equations

Option.isSome _fun_discr = match _fun_discr with | some val => true | none => false

@[inline]

def Option.isNone {α : Type u_1} :

Option α → Bool

Equations

Option.isNone _fun_discr = match _fun_discr with | some val => false | none => true

@[inline]

def Option.isEqSome {α : Type u_1} [inst : BEq α] :

Option α → α → Bool

Equations

Option.isEqSome _fun_discr _fun_discr = match _fun_discr, _fun_discr with | some a, b => a == b | none, x => false

@[inline]

def Option.bind {α : Type u_1} {β : Type u_2} :

Option α → (α → Option β) → Option β

Equations

Option.bind _fun_discr _fun_discr = match _fun_discr, _fun_discr with | none, x => none | some a, b => b a

@[inline]

def Option.map {α : Type u_1} {β : Type u_2} (f : α → β) (o : Option α) :

Equations

Option.map f o = Option.bind o (some ∘ f)

@[inline]

def Option.mapM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (f : α → m β) (o : Option α) :

m (Option β)

Equations

Option.mapM f o = match o with | some a => do let a ← f a pure (some a) | x => pure none

theorem Option.map_id {α : Type u_1} :

Option.map id = id

instance Option.instFunctorOption :

Equations

Option.instFunctorOption = { map := fun {α β} => Option.map, mapConst := fun {α β} => Option.map ∘ Function.const β }

@[inline]

def Option.filter {α : Type u_1} (p : α → Bool) :

Option α → Option α

Equations

Option.filter p _fun_discr = match _fun_discr with | some a => if p a = true then some a else none | none => none

@[inline]

def Option.all {α : Type u_1} (p : α → Bool) :

Option α → Bool

Equations

Option.all p _fun_discr = match _fun_discr with | some a => p a | none => true

@[inline]

def Option.any {α : Type u_1} (p : α → Bool) :

Option α → Bool

Equations

Option.any p _fun_discr = match _fun_discr with | some a => p a | none => false

@[macroInline]

def Option.orElse {α : Type u_1} :

Option α → (Unit → Option α) → Option α

Equations

Option.orElse _fun_discr _fun_discr = match _fun_discr, _fun_discr with | some a, x => some a | none, b => b ()

instance Option.instOrElseOption {α : Type u_1} :

OrElse (Option α)

Equations

Option.instOrElseOption = { orElse := Option.orElse }

@[inline]

noncomputable def Option.lt {α : Type u_1} (r : α → α → Prop) :

Option α → Option α → Prop

Equations

Option.lt r _fun_discr _fun_discr = match _fun_discr, _fun_discr with | none, some val => True | some x, some y => r x y | x, x_1 => False

instance Option.instDecidableRelOptionLt {α : Type u_1} (r : α → α → Prop) [s : DecidableRel r] :

DecidableRel (Option.lt r)

Equations

Option.instDecidableRelOptionLt r _fun_discr _fun_discr = match _fun_discr, _fun_discr with | none, some val => isTrue trivial | some x, some y => s x y | some val, none => isFalse not_false | none, none => isFalse not_false

instance instDecidableEqOption :

{α : Type u_1} → [inst : DecidableEq α] → DecidableEq (Option α)

Equations

instDecidableEqOption = [anonymous]

instance instBEqOption :

{α : Type u_1} → [inst : BEq α] → BEq (Option α)

Equations

instBEqOption = { beq := [anonymous] }

instance instLTOption {α : Type u_1} [inst : LT α] :

Equations

instLTOption = { lt := Option.lt fun a a_1 => a < a_1 }

instance instFunctorOption :

Equations

instFunctorOption = { map := fun {α β} => Option.map, mapConst := fun {α β} => Option.map ∘ Function.const β }

instance instMonadOption :

Equations

instMonadOption = Monad.mk

instance instAlternativeOption :

Alternative Option

Equations

instAlternativeOption = Alternative.mk (fun {α} => none) fun {α} => Option.orElse

def liftOption {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Alternative m] :

Option α → m α

Equations

liftOption _fun_discr = match _fun_discr with | some a => pure a | none => failure

@[inline]

def Option.tryCatch {α : Type u_1} (x : Option α) (handle : Unit → Option α) :

Equations

Option.tryCatch x handle = match x with | some val => x | none => handle ()

instance instMonadExceptOfUnitOption :

MonadExceptOf Unit Option

Equations

instMonadExceptOfUnitOption = { throw := fun {α} x => none, tryCatch := fun {α} => Option.tryCatch }