Module `0x1::Option`

This module defines the Option type and its methods to represent and handle an optional value.

Struct Option
Constants
Function none
Function some
Function is_none
Function is_some
Function contains
Function borrow
Function borrow_with_default
Function get_with_default
Function fill
Function extract
Function borrow_mut
Function swap
Function destroy_with_default
Function destroy_some
Function destroy_none
Module Specification
- Helper Schema

<pre><code>use <a href="Errors.md#0x1_Errors">0x1::Errors</a>; use <a href="Vector.md#0x1_Vector">0x1::Vector</a>; </code></pre>

Struct `Option`

Abstraction of a value that may or may not be present. Implemented with a vector of size zero or one because Move bytecode does not have ADTs.

<pre><code>struct <a href="Option.md#0x1_Option">Option</a><Element> has copy, drop, store </code></pre> <details> <summary>Fields</summary> <dl> <dt> <code>vec: vector<Element></code> </dt> <dd> </dd> </dl> </details> <details> <summary>Specification</summary>

The size of vector is always less than equal to 1 because it's 0 for "none" or 1 for "some".

<pre><code>invariant len(vec) <= 1; </code></pre> </details>

Constants

The <code><a href="Option.md#0x1_Option">Option</a></code> is in an invalid state for the operation attempted. The <code><a href="Option.md#0x1_Option">Option</a></code> is <code>Some</code> while it should be <code>None</code>.

<pre><code>const <a href="Option.md#0x1_Option_EOPTION_IS_SET">EOPTION_IS_SET</a>: u64 = 0; </code></pre>

<pre><code>const <a href="Option.md#0x1_Option_EOPTION_NOT_SET">EOPTION_NOT_SET</a>: u64 = 1; </code></pre>

Function `none`

Return an empty <code><a href="Option.md#0x1_Option">Option</a></code>

<pre><code>public fun <a href="Option.md#0x1_Option_none">none</a><Element>(): <a href="Option.md#0x1_Option_Option">Option::Option</a><Element> </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Option.md#0x1_Option_none">none</a><Element>(): <a href="Option.md#0x1_Option">Option</a><Element> { <a href="Option.md#0x1_Option">Option</a> { vec: <a href="Vector.md#0x1_Vector_empty">Vector::empty</a>() } } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; aborts_if false; ensures result == <a href="Option.md#0x1_Option_spec_none">spec_none</a><Element>(); </code></pre>

<pre><code>fun <a href="Option.md#0x1_Option_spec_none">spec_none</a><Element>(): <a href="Option.md#0x1_Option">Option</a><Element> { <a href="Option.md#0x1_Option">Option</a>{ vec: vec() } } </code></pre> </details>

Function `some`

Return an <code><a href="Option.md#0x1_Option">Option</a></code> containing <code>e</code>

<pre><code>public fun <a href="Option.md#0x1_Option_some">some</a><Element>(e: Element): <a href="Option.md#0x1_Option_Option">Option::Option</a><Element> </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Option.md#0x1_Option_some">some</a><Element>(e: Element): <a href="Option.md#0x1_Option">Option</a><Element> { <a href="Option.md#0x1_Option">Option</a> { vec: <a href="Vector.md#0x1_Vector_singleton">Vector::singleton</a>(e) } } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; aborts_if false; ensures result == <a href="Option.md#0x1_Option_spec_some">spec_some</a>(e); </code></pre>

<pre><code>fun <a href="Option.md#0x1_Option_spec_some">spec_some</a><Element>(e: Element): <a href="Option.md#0x1_Option">Option</a><Element> { <a href="Option.md#0x1_Option">Option</a>{ vec: vec(e) } } </code></pre> </details>

Function `is_none`

Return true if <code>t</code> does not hold a value

<pre><code>public fun <a href="Option.md#0x1_Option_is_none">is_none</a><Element>(t: &<a href="Option.md#0x1_Option_Option">Option::Option</a><Element>): bool </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Option.md#0x1_Option_is_none">is_none</a><Element>(t: &<a href="Option.md#0x1_Option">Option</a><Element>): bool { <a href="Vector.md#0x1_Vector_is_empty">Vector::is_empty</a>(&t.vec) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; aborts_if false; ensures result == <a href="Option.md#0x1_Option_is_none">is_none</a>(t); </code></pre> </details>

Function `is_some`

Return true if <code>t</code> holds a value

<pre><code>public fun <a href="Option.md#0x1_Option_is_some">is_some</a><Element>(t: &<a href="Option.md#0x1_Option_Option">Option::Option</a><Element>): bool </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Option.md#0x1_Option_is_some">is_some</a><Element>(t: &<a href="Option.md#0x1_Option">Option</a><Element>): bool { !<a href="Vector.md#0x1_Vector_is_empty">Vector::is_empty</a>(&t.vec) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; aborts_if false; ensures result == <a href="Option.md#0x1_Option_is_some">is_some</a>(t); </code></pre> </details>

Function `contains`

Return true if the value in <code>t</code> is equal to <code>e_ref</code> Always returns <code>false</code> if <code>t</code> does not hold a value

<pre><code>public fun <a href="Option.md#0x1_Option_contains">contains</a><Element>(t: &<a href="Option.md#0x1_Option_Option">Option::Option</a><Element>, e_ref: &Element): bool </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Option.md#0x1_Option_contains">contains</a><Element>(t: &<a href="Option.md#0x1_Option">Option</a><Element>, e_ref: &Element): bool { <a href="Vector.md#0x1_Vector_contains">Vector::contains</a>(&t.vec, e_ref) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; aborts_if false; ensures result == <a href="Option.md#0x1_Option_spec_contains">spec_contains</a>(t, e_ref); </code></pre>

<pre><code>fun <a href="Option.md#0x1_Option_spec_contains">spec_contains</a><Element>(t: <a href="Option.md#0x1_Option">Option</a><Element>, e: Element): bool { <a href="Option.md#0x1_Option_is_some">is_some</a>(t) && <a href="Option.md#0x1_Option_borrow">borrow</a>(t) == e } </code></pre> </details>

Function `borrow`

Return an immutable reference to the value inside <code>t</code> Aborts if <code>t</code> does not hold a value

<pre><code>public fun <a href="Option.md#0x1_Option_borrow">borrow</a><Element>(t: &<a href="Option.md#0x1_Option_Option">Option::Option</a><Element>): &Element </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Option.md#0x1_Option_borrow">borrow</a><Element>(t: &<a href="Option.md#0x1_Option">Option</a><Element>): &Element { assert(<a href="Option.md#0x1_Option_is_some">is_some</a>(t), <a href="Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="Option.md#0x1_Option_EOPTION_NOT_SET">EOPTION_NOT_SET</a>)); <a href="Vector.md#0x1_Vector_borrow">Vector::borrow</a>(&t.vec, 0) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; include <a href="Option.md#0x1_Option_AbortsIfNone">AbortsIfNone</a><Element>; ensures result == <a href="Option.md#0x1_Option_borrow">borrow</a>(t); </code></pre> </details>

Function `borrow_with_default`

Return a reference to the value inside <code>t</code> if it holds one Return <code>default_ref</code> if <code>t</code> does not hold a value

<pre><code>public fun <a href="Option.md#0x1_Option_borrow_with_default">borrow_with_default</a><Element>(t: &<a href="Option.md#0x1_Option_Option">Option::Option</a><Element>, default_ref: &Element): &Element </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Option.md#0x1_Option_borrow_with_default">borrow_with_default</a><Element>(t: &<a href="Option.md#0x1_Option">Option</a><Element>, default_ref: &Element): &Element { let vec_ref = &t.vec; if (<a href="Vector.md#0x1_Vector_is_empty">Vector::is_empty</a>(vec_ref)) default_ref else <a href="Vector.md#0x1_Vector_borrow">Vector::borrow</a>(vec_ref, 0) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; aborts_if false; ensures result == (if (<a href="Option.md#0x1_Option_is_some">is_some</a>(t)) <a href="Option.md#0x1_Option_borrow">borrow</a>(t) else default_ref); </code></pre> </details>

Function `get_with_default`

Return the value inside <code>t</code> if it holds one Return <code>default</code> if <code>t</code> does not hold a value

<pre><code>public fun <a href="Option.md#0x1_Option_get_with_default">get_with_default</a><Element: copy, drop>(t: &<a href="Option.md#0x1_Option_Option">Option::Option</a><Element>, default: Element): Element </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Option.md#0x1_Option_get_with_default">get_with_default</a><Element: copy + drop>( t: &<a href="Option.md#0x1_Option">Option</a><Element>, default: Element, ): Element { let vec_ref = &t.vec; if (<a href="Vector.md#0x1_Vector_is_empty">Vector::is_empty</a>(vec_ref)) default else *<a href="Vector.md#0x1_Vector_borrow">Vector::borrow</a>(vec_ref, 0) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; aborts_if false; ensures result == (if (<a href="Option.md#0x1_Option_is_some">is_some</a>(t)) <a href="Option.md#0x1_Option_borrow">borrow</a>(t) else default); </code></pre> </details>

Function `fill`

Convert the none option <code>t</code> to a some option by adding <code>e</code>. Aborts if <code>t</code> already holds a value

<pre><code>public fun <a href="Option.md#0x1_Option_fill">fill</a><Element>(t: &mut <a href="Option.md#0x1_Option_Option">Option::Option</a><Element>, e: Element) </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Option.md#0x1_Option_fill">fill</a><Element>(t: &mut <a href="Option.md#0x1_Option">Option</a><Element>, e: Element) { let vec_ref = &mut t.vec; if (<a href="Vector.md#0x1_Vector_is_empty">Vector::is_empty</a>(vec_ref)) <a href="Vector.md#0x1_Vector_push_back">Vector::push_back</a>(vec_ref, e) else abort <a href="Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="Option.md#0x1_Option_EOPTION_IS_SET">EOPTION_IS_SET</a>) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; aborts_if <a href="Option.md#0x1_Option_is_some">is_some</a>(t) with <a href="Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; ensures <a href="Option.md#0x1_Option_is_some">is_some</a>(t); ensures <a href="Option.md#0x1_Option_borrow">borrow</a>(t) == e; </code></pre> </details>

Function `extract`

Convert a <code>some</code> option to a <code>none</code> by removing and returning the value stored inside <code>t</code> Aborts if <code>t</code> does not hold a value

<pre><code>public fun <a href="Option.md#0x1_Option_extract">extract</a><Element>(t: &mut <a href="Option.md#0x1_Option_Option">Option::Option</a><Element>): Element </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Option.md#0x1_Option_extract">extract</a><Element>(t: &mut <a href="Option.md#0x1_Option">Option</a><Element>): Element { assert(<a href="Option.md#0x1_Option_is_some">is_some</a>(t), <a href="Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="Option.md#0x1_Option_EOPTION_NOT_SET">EOPTION_NOT_SET</a>)); <a href="Vector.md#0x1_Vector_pop_back">Vector::pop_back</a>(&mut t.vec) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; include <a href="Option.md#0x1_Option_AbortsIfNone">AbortsIfNone</a><Element>; ensures result == <a href="Option.md#0x1_Option_borrow">borrow</a>(old(t)); ensures <a href="Option.md#0x1_Option_is_none">is_none</a>(t); </code></pre> </details>

Function `borrow_mut`

Return a mutable reference to the value inside <code>t</code> Aborts if <code>t</code> does not hold a value

<pre><code>public fun <a href="Option.md#0x1_Option_borrow_mut">borrow_mut</a><Element>(t: &mut <a href="Option.md#0x1_Option_Option">Option::Option</a><Element>): &mut Element </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Option.md#0x1_Option_borrow_mut">borrow_mut</a><Element>(t: &mut <a href="Option.md#0x1_Option">Option</a><Element>): &mut Element { assert(<a href="Option.md#0x1_Option_is_some">is_some</a>(t), <a href="Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="Option.md#0x1_Option_EOPTION_NOT_SET">EOPTION_NOT_SET</a>)); <a href="Vector.md#0x1_Vector_borrow_mut">Vector::borrow_mut</a>(&mut t.vec, 0) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; include <a href="Option.md#0x1_Option_AbortsIfNone">AbortsIfNone</a><Element>; ensures result == <a href="Option.md#0x1_Option_borrow">borrow</a>(t); </code></pre> </details>

Function `swap`

Swap the old value inside <code>t</code> with <code>e</code> and return the old value Aborts if <code>t</code> does not hold a value

<pre><code>public fun <a href="Option.md#0x1_Option_swap">swap</a><Element>(t: &mut <a href="Option.md#0x1_Option_Option">Option::Option</a><Element>, e: Element): Element </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Option.md#0x1_Option_swap">swap</a><Element>(t: &mut <a href="Option.md#0x1_Option">Option</a><Element>, e: Element): Element { assert(<a href="Option.md#0x1_Option_is_some">is_some</a>(t), <a href="Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="Option.md#0x1_Option_EOPTION_NOT_SET">EOPTION_NOT_SET</a>)); let vec_ref = &mut t.vec; let old_value = <a href="Vector.md#0x1_Vector_pop_back">Vector::pop_back</a>(vec_ref); <a href="Vector.md#0x1_Vector_push_back">Vector::push_back</a>(vec_ref, e); old_value } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; include <a href="Option.md#0x1_Option_AbortsIfNone">AbortsIfNone</a><Element>; ensures result == <a href="Option.md#0x1_Option_borrow">borrow</a>(old(t)); ensures <a href="Option.md#0x1_Option_is_some">is_some</a>(t); ensures <a href="Option.md#0x1_Option_borrow">borrow</a>(t) == e; </code></pre> </details>

Function `destroy_with_default`

Destroys <code>t.</code> If <code>t</code> holds a value, return it. Returns <code>default</code> otherwise

<pre><code>public fun <a href="Option.md#0x1_Option_destroy_with_default">destroy_with_default</a><Element: drop>(t: <a href="Option.md#0x1_Option_Option">Option::Option</a><Element>, default: Element): Element </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Option.md#0x1_Option_destroy_with_default">destroy_with_default</a><Element: drop>(t: <a href="Option.md#0x1_Option">Option</a><Element>, default: Element): Element { let <a href="Option.md#0x1_Option">Option</a> { vec } = t; if (<a href="Vector.md#0x1_Vector_is_empty">Vector::is_empty</a>(&mut vec)) default else <a href="Vector.md#0x1_Vector_pop_back">Vector::pop_back</a>(&mut vec) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; aborts_if false; ensures result == (if (<a href="Option.md#0x1_Option_is_some">is_some</a>(t)) <a href="Option.md#0x1_Option_borrow">borrow</a>(t) else default); </code></pre> </details>

Function `destroy_some`

Unpack <code>t</code> and return its contents Aborts if <code>t</code> does not hold a value

<pre><code>public fun <a href="Option.md#0x1_Option_destroy_some">destroy_some</a><Element>(t: <a href="Option.md#0x1_Option_Option">Option::Option</a><Element>): Element </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Option.md#0x1_Option_destroy_some">destroy_some</a><Element>(t: <a href="Option.md#0x1_Option">Option</a><Element>): Element { assert(<a href="Option.md#0x1_Option_is_some">is_some</a>(&t), <a href="Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="Option.md#0x1_Option_EOPTION_NOT_SET">EOPTION_NOT_SET</a>)); let <a href="Option.md#0x1_Option">Option</a> { vec } = t; let elem = <a href="Vector.md#0x1_Vector_pop_back">Vector::pop_back</a>(&mut vec); <a href="Vector.md#0x1_Vector_destroy_empty">Vector::destroy_empty</a>(vec); elem } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; include <a href="Option.md#0x1_Option_AbortsIfNone">AbortsIfNone</a><Element>; ensures result == <a href="Option.md#0x1_Option_borrow">borrow</a>(t); </code></pre> </details>

Function `destroy_none`

Unpack <code>t</code> Aborts if <code>t</code> holds a value

<pre><code>public fun <a href="Option.md#0x1_Option_destroy_none">destroy_none</a><Element>(t: <a href="Option.md#0x1_Option_Option">Option::Option</a><Element>) </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Option.md#0x1_Option_destroy_none">destroy_none</a><Element>(t: <a href="Option.md#0x1_Option">Option</a><Element>) { assert(<a href="Option.md#0x1_Option_is_none">is_none</a>(&t), <a href="Errors.md#0x1_Errors_invalid_argument">Errors::invalid_argument</a>(<a href="Option.md#0x1_Option_EOPTION_IS_SET">EOPTION_IS_SET</a>)); let <a href="Option.md#0x1_Option">Option</a> { vec } = t; <a href="Vector.md#0x1_Vector_destroy_empty">Vector::destroy_empty</a>(vec) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>pragma opaque; aborts_if <a href="Option.md#0x1_Option_is_some">is_some</a>(t) with <a href="Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; </code></pre> </details>

Module Specification

<pre><code>pragma aborts_if_is_strict; </code></pre>

Helper Schema

<pre><code>schema <a href="Option.md#0x1_Option_AbortsIfNone">AbortsIfNone</a><Element> { t: <a href="Option.md#0x1_Option">Option</a><Element>; aborts_if <a href="Option.md#0x1_Option_is_none">is_none</a>(t) with <a href="Errors.md#0x1_Errors_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; } </code></pre>

Module `0x1::Option`

Module 0x1::Option

Struct Option

Constants

Function none

Function some

Function is_none

Function is_some

Function contains

Function borrow

Function borrow_with_default

Function get_with_default

Function fill

Function extract

Function borrow_mut

Function swap

Function destroy_with_default

Function destroy_some

Function destroy_none

Module Specification

Helper Schema

Module `0x1::Option`

Struct `Option`

Function `none`

Function `some`

Function `is_none`

Function `is_some`

Function `contains`

Function `borrow`

Function `borrow_with_default`

Function `get_with_default`

Function `fill`

Function `extract`

Function `borrow_mut`

Function `swap`

Function `destroy_with_default`

Function `destroy_some`

Function `destroy_none`