Skip to main content

Option

inductive Option[T] {
    none
    some(T)
}

Optional values that can either contain a value of type T or be empty. Useful for representing values that may or may not exist.

GitHub

bind​

define bind[U](self, f: T -> Option[U]) -> Option[U] {
    option_bind(self, f)
}

The result of applying an optional-value function to this optional value.

get_or_else​

define get_or_else(self, fallback: T) -> T {
    option_get_or_else(self, fallback)
}

The contained value, or the given fallback when there is no contained value.

is_none​

let is_none: Option[T] -> Bool = option_is_none

True if the optional value contains no element.

is_some​

let is_some: Option[T] -> Bool = option_is_some

True if the optional value contains an element.

map​

define map[U](self, f: T -> U) -> Option[U] {
    option_map(self, f)
}

The image of this optional value under a function.

match​

Option.match: (Option[T*], R*, T* -> R*) -> R*

none​

Option.none: Option[T]

Option.none represents the absence of a value.

some​

Option.some: T -> Option[T]

Option.some(value) represents the presence of a value.