Option
Reference for mo:core/Option in the core library.
Option helpers preserve null/present shape in their contracts. Higher-order
helpers such as map, chain, equal, and compare may require pure or
contracted callbacks in verification-heavy code.
Import
mo:core/Option
Status
- Runtime module
Public API
Functions
get<T>(x : ?T, default : T) : T
Reads the requested value from the structure.
Contract
ensures result == (switch x { case null { default }; case (?value) { value } });
Use when: reading this value is part of an implementation or postcondition.
getMapped<A, B>(x : ?A, f : A -> B, default : B) : B
Reads the requested value from the structure.
Contract
ensures x == null ==> result == default;
Use when: reading this value is part of an implementation or postcondition.
map<A, B>(x : ?A, f : A -> B) : ?B
Transforms the contained values with the supplied function while preserving the documented shape.
Contract
ensures x == null ==> result == null;
ensures x != null ==> result != null;
ensures result == null ==> x == null;
Use when: code or specifications need this operation with the documented contract.
forEach<A>(x : ?A, f : A -> ()) : ()
Runs the supplied callback only for the matching contained value.
Use when: code or specifications need this operation with the documented contract.
apply<A, B>(x : ?A, f : ?(A -> B)) : ?B
Applies an optional function to an optional value when both are present.
Contract
ensures (x == null or f == null) ==> result == null;
ensures (x != null and f != null) ==> result != null;
ensures result == null ==> (x == null or f == null);
Use when: code or specifications need this operation with the documented contract.
chain<A, B>(x : ?A, f : A -> ?B) : ?B
Sequences a fallible or optional computation without adding an extra nesting layer.
Contract
ensures x == null ==> result == null;
ensures result != null ==> x != null;
Use when: code or specifications need this operation with the documented contract.
flatten<A>(x : ??A) : ?A
Removes one layer of nested Option or Result structure.
Contract
ensures result == (switch x { case null { null }; case (?value) { value } });
Use when: code or specifications need this operation with the documented contract.
some<A>(x : A) : ?A
Wraps a value in a present option.
Contract
ensures result == ?x;
Use when: code or specifications need this operation with the documented contract.
isSome<A>(x : ?A) : Bool
Checks the predicate described by the return contract.
Contract
ensures result == (x != null);
Use when: a branch condition or contract needs this predicate as a named fact.
isNull<A>(x : ?A) : Bool
Checks the predicate described by the return contract.
Contract
ensures result == (x == null);
Use when: a branch condition or contract needs this predicate as a named fact.
equal<A>(x : ?A, y : ?A, eq : (A, A) -> Bool) : Bool
Compares the supplied values and relates the result to the underlying order.
Contract
ensures (x == null and y == null) ==> result;
ensures (x == null and y != null) ==> not result;
ensures (x != null and y == null) ==> not result;
Use when: code or contracts need an explicit comparison helper instead of an operator.
compare<A>(x : ?A, y : ?A, cmp : (A, A) -> Types.Order) : Types.Order
Compares the supplied values and relates the result to the underlying order.
Contract
ensures (x == null and y == null) ==> result == #equal;
ensures (x == null and y != null) ==> result == #less;
ensures (x != null and y == null) ==> result == #greater;
Use when: code or contracts need an explicit comparison helper instead of an operator.
unwrap<T>(x : ?T) : T
Extracts the present option value, requiring the option to be non-null.
Contract
requires x != null;
ensures switch x { case (?value) { result == value }; case null { true } };
Use when: code or specifications need this operation with the documented contract.
toText<A>(x : ?A, toText : A -> Text) : Text
Converts between the module type and the target representation.
Contract
ensures x == null ==> result == "null";
ensures x != null ==> result != "null";
ensures result == "null" ==> x == null;
Use when: crossing between this module's value and another representation.
Summary
- Runtime module under
mo:core/Option. - Exposes 14 public functions.