def
Option.toMonad
{m : Type u_1 → Type u_2}
{α : Type u_1}
[inst : Monad m]
[inst : Alternative m]
:
Option α → m α
Equations
- Option.toMonad x = match x with | none => failure | some a => pure a
@[inline]
Equations
- Option.toBool x = match x with | some x => true | none => false
@[inline]
Equations
- Option.isSome x = match x with | some x => true | none => false
@[inline]
Equations
- Option.isNone x = match x with | some x => false | none => true
@[inline]
Equations
- Option.isEqSome x x = match x, x with | some a, b => a == b | none, x => false
@[inline]
Equations
- Option.bind x x = match x, x with | none, b => none | some a, b => b a
@[inline]
Equations
- Option.map f o = Option.bind o (some ∘ f)
Equations
- Option.instFunctorOption = { map := fun {α β} => Option.map, mapConst := fun {α β} => Option.map ∘ Function.const β }
@[inline]
Equations
- Option.all p x = match x with | some a => p a | none => true
@[inline]
Equations
- Option.any p x = match x with | some a => p a | none => false
@[macroInline]
Equations
- Option.orElse x x = match x, x with | some a, x => some a | none, b => b ()
Equations
- Option.instOrElseOption = { orElse := Option.orElse }
Equations
- instDecidableEqOption = [anonymous]