@[inline]

def Data.Maybe.maybe {β : Sort u_1} {α : Type u_2} (b : β) (f : α → β) : Option α → β

Case analysis on Option (Haskell's maybe).

$$\text{maybe}(b, f, \text{none}) = b, \quad \text{maybe}(b, f, \text{some}\;a) = f(a)$$

Equations

• Data.Maybe.maybe b f none = b
• Data.Maybe.maybe b f (some a) = f a

@[inline]

def Data.Maybe.fromMaybe {α : Type u_1} (d : α) : Option α → α

Extract from Option with a default (Haskell's fromMaybe).

$$\text{fromMaybe}(d, \text{none}) = d, \quad \text{fromMaybe}(d, \text{some}\;a) = a$$

Equations

• Data.Maybe.fromMaybe d none = d
• Data.Maybe.fromMaybe d (some a) = a

@[inline]

def Data.Maybe.isJust {α : Type u_1} : Option α → Bool

Test if some (Haskell's isJust).

Equations

• Data.Maybe.isJust = Option.isSome

@[inline]

def Data.Maybe.isNothing {α : Type u_1} : Option α → Bool

Test if none (Haskell's isNothing).

Equations

• Data.Maybe.isNothing = Option.isNone

def Data.Maybe.catMaybes {α : Type u_1} : List (Option α) → List α

Collect some values from a list (Haskell's catMaybes).

$$\text{catMaybes}([x_1, \ldots, x_n]) = [a \mid x_i = \text{some}\;a]$$

Equations

• Data.Maybe.catMaybes [] = []
• Data.Maybe.catMaybes (none :: rest) = Data.Maybe.catMaybes rest
• Data.Maybe.catMaybes (some a :: rest) = a :: Data.Maybe.catMaybes rest

def Data.Maybe.mapMaybe {α : Type u_1} {β : Type u_2} (f : α → Option β) : List α → List β

Map and filter in one pass (Haskell's mapMaybe).

$$\text{mapMaybe}(f, xs) = \text{catMaybes}(\text{map}\;f\;xs)$$

Equations

• Data.Maybe.mapMaybe f [] = []
• Data.Maybe.mapMaybe f (x_1 :: rest) = match f x_1 with | none => Data.Maybe.mapMaybe f rest | some b => b :: Data.Maybe.mapMaybe f rest

@[inline]

def Data.Maybe.listToMaybe {α : Type u_1} : List α → Option α

First element or none (Haskell's listToMaybe).

Equations

• Data.Maybe.listToMaybe [] = none
• Data.Maybe.listToMaybe (x_1 :: rest) = some x_1

@[inline]

def Data.Maybe.maybeToList {α : Type u_1} : Option α → List α

Option to singleton or empty list (Haskell's maybeToList).

Equations

• Data.Maybe.maybeToList none = []
• Data.Maybe.maybeToList (some a) = [a]

def Data.Maybe.fromJust {α : Type u_1} (o : Option α) : o.isSome = true → α

Safe unwrap with proof that value is some (Haskell's fromJust made safe).

$$\text{fromJust}(\text{some}\;a, \_) = a$$

Equations

• Data.Maybe.fromJust (some a) x_2 = a

theorem Data.Maybe.maybe_none {β : Sort u_1} {α : Type u_2} (b : β) (f : α → β) : maybe b f none = b

maybe on none returns the default.

theorem Data.Maybe.maybe_some {β : Sort u_1} {α : Type u_2} (b : β) (f : α → β) (a : α) : maybe b f (some a) = f a

maybe on some applies the function.

theorem Data.Maybe.fromMaybe_none {α : Type u_1} (d : α) : fromMaybe d none = d

fromMaybe on none returns the default.

theorem Data.Maybe.fromMaybe_some {α : Type u_1} (d a : α) : fromMaybe d (some a) = a

fromMaybe on some extracts the value.

theorem Data.Maybe.catMaybes_nil {α : Type u_1} : catMaybes [] = []

catMaybes of empty list is empty.

theorem Data.Maybe.mapMaybe_nil {α : Type u_1} {β : Type u_2} (f : α → Option β) : mapMaybe f [] = []

mapMaybe of empty list is empty.

theorem Data.Maybe.maybeToList_listToMaybe {α : Type u_1} (o : Option α) : listToMaybe (maybeToList o) = o

maybeToList / listToMaybe roundtrip.

theorem Data.Maybe.catMaybes_eq_mapMaybe_id {α : Type u_1} (l : List (Option α)) : catMaybes l = mapMaybe id l

catMaybes is mapMaybe id.