Skip to main content

ghost/Multiset

Reference for mo:core/ghost/Multiset 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/Multiset

Status​

  • Spec-only module

Public API​

Functions​

empty<T>() : Multiset<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) : Multiset<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.

card<T>(m : Multiset<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.

contains<T>(e : T, m : Multiset<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.

count<T>(m : Multiset<T>, e : 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.

union<T>(m : Multiset<T>, n : Multiset<T>) : Multiset<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.

intersect<T>(m : Multiset<T>, n : Multiset<T>) : Multiset<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.

minus<T>(m : Multiset<T>, n : Multiset<T>) : Multiset<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.

Summary​

  • Spec-only module under mo:core/ghost/Multiset.
  • Exposes 8 public functions.