Skip to main content

ghost/Set

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

Status​

  • Spec-only module

Public API​

Functions​

empty<T>() : Set<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) : Set<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>(s : Set<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, s : Set<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.

union<T>(s : Set<T>, t : Set<T>) : Set<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>(s : Set<T>, t : Set<T>) : Set<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>(s : Set<T>, t : Set<T>) : Set<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.

subset<T>(s : Set<T>, t : Set<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/Set.
  • Exposes 8 public functions.