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.
A simple tao struct containing a vector of resources.
struct Tao<Content> has store, key
Fields
-
content: vector<Content>
Create a new tao, with the static set of resources inside it.
public fun wrap<Content>(content: vector<Content>): Folder::Tao<Content>
Implementation
Specification
ensures result == Tao<Content> { content: content };
Immutable read-only reference to the vector containing resources.
public fun read<Content>(tao: &Folder::Tao<Content>): &vector<Content>
Implementation
Specification
ensures result == tao.content;
Destroy the tao, and return the static set of resources inside it.
public fun unwrap<Content>(tao: Folder::Tao<Content>): vector<Content>
Implementation
Specification
ensures result == tao.content;
pragma aborts_if_is_strict;