Init.Data.Option.Basic

source

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

source

@[inline]

def Option.toBool {α : Type u_1} :

Option α → Bool

Equations

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

source

@[inline]

def Option.isSome {α : Type u_1} :

Option α → Bool

Equations

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

source

@[inline]

def Option.isNone {α : Type u_1} :

Option α → Bool

Equations

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

source

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

source

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

source

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

source

theorem Option.map_id {α : Type u_1} :

Option.map id = id

source

instance Option.instFunctorOption:

Functor Option

Equations

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

source

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

source

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

source

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

source

@[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 ()

source

instance Option.instOrElseOption {α : Type u_1} :

OrElse (Option α)

Equations

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

source

@[inline]

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

source

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

DecidableRel (Option.lt r)

Equations

One or more equations did not get rendered due to their size.

source

instance instDecidableEqOption:

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

Equations

instDecidableEqOption = [anonymous]

source

instance instBEqOption:

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

Equations

instBEqOption = { beq := [anonymous] }

source

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

LT (Option α)

Equations

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

source

instance instFunctorOption:

Functor Option

Equations

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

source

instance instMonadOption:

Monad Option

Equations

instMonadOption = Monad.mk

source

instance instAlternativeOption:

Alternative Option

Equations

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

source

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

source

@[inline]

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

Option α

Equations

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

source

instance instMonadExceptOfUnitOption:

MonadExceptOf Unit Option

Equations

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