- 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;