Skip to main content

Iter

Reference for mo:core/Iter in the core library.

Iter<T> is the standard { next : () -> ?T } iterator shape. The Spec module gives ghost predicates for membership-style contracts, while runtime iteration still consumes mutable iterator state.

Import​

mo:core/Iter

Status​

  • Runtime module

Public API​

Types​

  • Iter

Modules​

  • Spec

Functions​

empty<T>() : Iter<T>​

Constructs the empty value for this module's data structure.

Contract

ensures forall<T>(pure func (k : T) : Bool = not Spec.contains<T>(result, k));

Use when: code or specifications need this operation with the documented contract.

singleton<T>(value : T) : Iter<T>​

Constructs a value containing exactly the supplied element or entry.

Contract

ensures Spec.contains<T>(result, value);
ensures forall<T>(pure func (k : T) : Bool = Spec.contains<T>(result, k) ==> k == value);
ensures forall<T>(pure func (k : T) : Bool = (k == value) ==> Spec.contains<T>(result, k));

Use when: code or specifications need this operation with the documented contract.

reverse<T>(iter : Iter<T>) : Iter<T>​

Materializes an iterator in reverse order.

Contract

ensures forall<T>(pure func (k : T) : Bool =
Spec.contains<T>(result, k) ==> Spec.contains<T>(iter, k));
ensures forall<T>(pure func (k : T) : Bool =
Spec.contains<T>(iter, k) ==> Spec.contains<T>(result, k));

Use when: code or specifications need this operation with the documented contract.

Spec Module​

Spec Functions​

contains<T>(iter : Types.Iter<T>, value : 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.

forall<T>(pred : T -> Bool) : 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​

  • Runtime module under mo:core/Iter.
  • Exposes 3 public functions.
  • Includes 2 spec helpers in Spec.