Module 0x2f66c09143acc52a85fec529a4e20c85::Folder

This tao is designed to contain a static array of resources. As with normal tao lifespan, the tao is created with a set of resources, and the same set will be returned when the tao is destroyed.

• Resource Tao
• Function wrap
• Function read
• Function unwrap

Resource Tao

A simple tao struct containing a vector of resources.

struct Tao<Content> has store, key

Fields

content: vector<Content>

Function wrap

Create a new tao, with the static set of resources inside it.

public fun wrap<Content>(content: vector<Content>): Folder::Tao<Content>

Implementation

public fun wrap<Content>(content: vector<Content>): Tao<Content> {
    Tao<Content> { content }
}

Specification

ensures result ==  Tao<Content> { content: content };

Function read

Immutable read-only reference to the vector containing resources.

public fun read<Content>(tao: &Folder::Tao<Content>): &vector<Content>

Implementation

public fun read<Content>(tao: &Tao<Content>): &vector<Content> {
    let Tao<Content> { content } = tao;

    content
}

Specification

ensures result == tao.content;

Function unwrap

Destroy the tao, and return the static set of resources inside it.

public fun unwrap<Content>(tao: Folder::Tao<Content>): vector<Content>

Implementation

public fun unwrap<Content>(tao: Tao<Content>): vector<Content> {
    let Tao<Content> { content } = tao;

    content
}

Specification

ensures result == tao.content;

pragma aborts_if_is_strict;