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: | None | Some: T. Unlike [] ∪ T, it neither collapses Opt@[] to [] nor flattens Opt@(Opt@T) to Opt@T. T is implicit, so Opt#Some 23 and Opt#None infer it; (Opt@Nat)#None gives it explicitly.

anx nom Opt {T: *} =
    | None
    | Some: T;

Operations

some_if

Wraps v into an option iff b holds.

anx lam some_if {T: *} (b: Bool, v: T): Opt@T = (Opt#None, Opt#Some v)#b;

is_some

Returns tt if the option contains a value.

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

unwrap_unsafe

Extracts the value without checking - undefined behavior for 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
        | None   => default
        | Some x => x;