The option Plugin

Table of Contents

• Dependencies
• Types
  • %option.Opt
• Constructors
  • %option.some
  • %option.none
• Operations
  • %option.is_some
  • %option.unwrap_unsafe
  • %option.unwrap_or

See also

mim::plug::option

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

Dependencies

plugin core;

Types

%option.Opt

The option type: [] ∪ T.

lam %option.Opt (T: *) : * = [] ∪ T;

Constructors

%option.some

Wraps a value into an option.

lam %option.some {T: *} (v: T) : %option.Opt T = v inj %option.Opt T;

%option.none

The empty option.

lam %option.none {T: *} : %option.Opt T = () inj %option.Opt T;

Operations

%option.is_some

Returns tt if the option contains a value.

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

%option.unwrap_unsafe

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

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

%option.unwrap_or

Extracts the value or returns default.

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