The vec Plugin

Table of Contents

• Dependencies
• Iterators
  • %vec.fold
• Scanning
  • %vec.scan
  • %vec.len
  • %vec.unique
• Modifiers
  • %vec.diff

See also

mim::plug::vec

Utilitly functions for arrays to behave them like vectors in other languages.

Dependencies

plugin core;
plugin refly;

Iterators

%vec.fold

Fold aka Reduction of the vector with f:

• %vec.fold.l f (init, (e1, ..., en)) is f (... (f (f (init, e1), e2)) ..., en).
• %vec.fold.r f ((e1, ..., en), init) is f (e1, f (e2, ... (f (en, init) ...))).

%vec.fold.l	%vec.fold.r

axm %vec.fold(l): {A E: *} → {n: Nat} → [f: [A, E] → A] → [A, «n; E»] → A, normalize_fold;
axm %vec.fold(r): {A E: *} → {n: Nat} → [f: [E, A] → A] → [«n; E», A] → A, normalize_fold;

Scanning

%vec.scan

Does the given predicate hold for all elements/at least one element?

axm %vec.scan(for_all, exists): {E: *} → {n: Nat} → [p: E → Bool] → «n; E» → Bool, normalize_scan;

%vec.len

Get length of vector.

lam %vec.len {n: Nat} {T: *} [«n; T»]: Nat = n;

%vec.unique

Checks whether all elements in the given vector are distinct from each other (using structural equivalence).

axm %vec.is_unique: {T: *} → {n: Nat} → «n; T» → Bool, normalize_is_unique;

Modifiers

%vec.diff

Removes elements from vector.

axm %vec.diff: {T: *}
             → {n m: Nat}
             → [«n; T», is: «m; Idx n»]
             → «%refly.check (%vec.is_unique is, %core.nat.sub (n, m), "given indices are not distinct"); T», normalize_diff;