ghost/Seq

Reference for mo:core/ghost/Seq in the core library.

This module is ghost-only: values are mathematical proof objects for contracts, ghost code, and lemmas. Operations are persistent and do not consume previous values; cardinalities and sequence lengths use verifier Int, so bridge to runtime Nat sizes explicitly when needed.

Import

mo:core/ghost/Seq

Status

• Spec-only module

Public API

Functions

empty<T>() : Seq<T>

Provides a ghost/spec-only abstraction for contracts and proofs.

Use when: Use in contracts, ghost code, or lemmas when the runtime value needs an abstract proof model.

singleton<T>(e : T) : Seq<T>

Provides a ghost/spec-only abstraction for contracts and proofs.

Use when: Use in contracts, ghost code, or lemmas when the runtime value needs an abstract proof model.

len<T>(s : Seq<T>) : Int

Provides a ghost/spec-only abstraction for contracts and proofs.

Use when: Use in contracts, ghost code, or lemmas when the runtime value needs an abstract proof model.

get<T>(s : Seq<T>, i : Int) : T

Provides a ghost/spec-only abstraction for contracts and proofs.

Use when: Use in contracts, ghost code, or lemmas when the runtime value needs an abstract proof model.

concat<T>(s : Seq<T>, t : Seq<T>) : Seq<T>

Provides a ghost/spec-only abstraction for contracts and proofs.

Use when: Use in contracts, ghost code, or lemmas when the runtime value needs an abstract proof model.

append<T>(s : Seq<T>, e : T) : Seq<T>

Provides a ghost/spec-only abstraction for contracts and proofs.

Use when: Use in contracts, ghost code, or lemmas when the runtime value needs an abstract proof model.

update<T>(s : Seq<T>, i : Int, v : T) : Seq<T>

Provides a ghost/spec-only abstraction for contracts and proofs.

Use when: Use in contracts, ghost code, or lemmas when the runtime value needs an abstract proof model.

take<T>(s : Seq<T>, n : Int) : Seq<T>

Provides a ghost/spec-only abstraction for contracts and proofs.

Use when: Use in contracts, ghost code, or lemmas when the runtime value needs an abstract proof model.

drop<T>(s : Seq<T>, n : Int) : Seq<T>

Provides a ghost/spec-only abstraction for contracts and proofs.

Use when: Use in contracts, ghost code, or lemmas when the runtime value needs an abstract proof model.

slice<T>(s : Seq<T>, i : Int, j : Int) : Seq<T>

Provides a ghost/spec-only abstraction for contracts and proofs.

Use when: Use in contracts, ghost code, or lemmas when the runtime value needs an abstract proof model.

contains<T>(e : T, s : Seq<T>) : Bool

Provides a ghost/spec-only abstraction for contracts and proofs.

Use when: Use in contracts, ghost code, or lemmas when the runtime value needs an abstract proof model.

sorted(s : Seq<Nat>) : Bool

Provides a ghost/spec-only abstraction for contracts and proofs.

Use when: Use in contracts, ghost code, or lemmas when the runtime value needs an abstract proof model.

permutes<T>(a : Seq<T>, b : Seq<T>) : Bool

Provides a ghost/spec-only abstraction for contracts and proofs.

Use when: Use in contracts, ghost code, or lemmas when the runtime value needs an abstract proof model.

Summary

• Spec-only module under mo:core/ghost/Seq.
• Exposes 13 public functions.