The option Plugin

See also

mim::plug::option

An optional value type: either a value of type T or nothing.

Dependencies

plugin core;

Types

Opt

The option type: [] ∪ T.

anx lam Opt (T: *) : * = [] ∪ T;

Constructors

some

Wraps a value into an option.

anx lam some {T: *} (v: T) : Opt T = v inj Opt T;

none

The empty option.

anx lam none (T: *) : Opt T = () inj Opt T;

some_if

Wraps v into an option iff b holds.

anx lam some_if {T: *} (b: Bool, v: T) : Opt T = (none T, some v)#b;

Operations

is_some

Returns tt if the option contains a value.

anx lam is_some {T: *} (o: Opt T) : Bool =
    match o with
        | _: T  => tt
        | _: [] => ff;

unwrap_unsafe

Extracts the value without checking - undefined behavior for option.none.

axm unwrap_unsafe: {T: *} → Opt T → T, normalize_unwrap_unsafe;

unwrap_or

Extracts the value or returns default.

anx lam unwrap_or {T: *} (o: Opt T) (default: T) : T =
    match o with
        | x: T  => x
        | _: [] => default;