# Documentation

Init.Data.Option.Basic

def Option.toMonad {m : Type u_1 → Type u_2} {α : Type u_1} [inst : ] [inst : ] :
m α
Equations
• = match x with | none => failure | some a => pure a
@[inline]
def Option.toBool {α : Type u_1} :
Bool
Equations
• = match x with | some val => true | none => false
@[inline]
def Option.isSome {α : Type u_1} :
Bool
Equations
• = match x with | some val => true | none => false
@[inline]
def Option.isNone {α : Type u_1} :
Bool
Equations
• = match x with | some val => false | none => true
@[inline]
def Option.isEqSome {α : Type u_1} [inst : BEq α] :
αBool
Equations
• = match x, x with | some a, b => a == b | none, x => false
@[inline]
def Option.bind {α : Type u_1} {β : Type u_2} :
(α) →
Equations
• = match x, x with | none, x => none | some a, b => b a
@[inline]
def Option.mapM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : ] (f : αm β) (o : ) :
m ()
Equations
• = match o with | some a => do let __do_lift ← f a pure (some __do_lift) | x => pure none
theorem Option.map_id {α : Type u_1} :
= id
@[inline]
def Option.filter {α : Type u_1} (p : αBool) :
Equations
• = match x with | some a => if p a = true then some a else none | none => none
@[inline]
def Option.all {α : Type u_1} (p : αBool) :
Bool
Equations
• = match x with | some a => p a | none => true
@[inline]
def Option.any {α : Type u_1} (p : αBool) :
Bool
Equations
• = match x with | some a => p a | none => false
@[macro_inline]
def Option.orElse {α : Type u_1} :
(Unit) →
Equations
• = match x, x with | some a, x => some a | none, b => b ()
instance Option.instOrElseOption {α : Type u_1} :
Equations
• Option.instOrElseOption = { orElse := Option.orElse }
@[inline]
def Option.lt {α : Type u_1} (r : ααProp) :
Prop
Equations
instance Option.instDecidableRelOptionLt {α : Type u_1} (r : ααProp) [s : ] :
Equations
• One or more equations did not get rendered due to their size.
def Option.merge {α : Type u_1} (fn : ααα) :

Take a pair of options and if they are both some, apply the given fn to produce an output. Otherwise act like orElse.

Equations
instance instDecidableEqOption :
{α : Type u_1} → [inst : ] →
Equations
• instDecidableEqOption = decEqOption✝
instance instBEqOption :
{α : Type u_1} → [inst : BEq α] → BEq ()
Equations
• instBEqOption = { beq := beqOption✝ }
instance instLTOption {α : Type u_1} [inst : LT α] :
LT ()
Equations
• instLTOption = { lt := Option.lt fun x x_1 => x < x_1 }
@[always_inline]
Equations
@[always_inline]