Std.Vector

View source →

Length-indexed vectors.

Vector(a, n) is a real indexed family checked by the dependent kernel. The length is the Nat index, not a runtime tuple field. Erasure leaves the compact constructor spine :empty / {:prepend, head, tail} while the type checker keeps every length relationship precise.

Functions

  • # fn all(a: Type, n: Nat, xs: Vector(a, n), pred: Function(a, Bool)) -> Bool
  • # fn any(a: Type, n: Nat, xs: Vector(a, n), pred: Function(a, Bool)) -> Bool
  • # fn append(a: Type, m: Nat, n: Nat, xs: Vector(a, m), ys: Vector(a, n)) -> Vector(a, plus(m, n))
  • # fn count(a: Type, n: Nat, xs: Vector(a, n)) -> Nat
  • # fn drop(a: Type, n: Nat, m: Nat, xs: Vector(a, plus(n, m))) -> Vector(a, m)

    Drop the first n elements of a vector of length plus(n, m), keeping the trailing m. Same convoy: with n refines xs, so the Z branch returns xs directly (plus(Z, m) reduces to m, matching the Vector(a, m) result) and the S(k) branch peels one element off the now-non-empty xs.

  • # fn find(a: Type, n: Nat, xs: Vector(a, n), pred: Function(a, Bool)) -> Option(a)

    First element satisfying pred, or None if there is none.

  • # fn foldl(a: Type, b: Type, n: Nat, xs: Vector(a, n), acc: b, f: Function(a, Function(b, b))) -> b
  • # fn foldr(a: Type, b: Type, n: Nat, xs: Vector(a, n), acc: b, f: Function(a, Function(b, b))) -> b
  • # fn from_list(a: Type, xs: List(a)) -> Sigma(n: Nat, Vector(a, n))

    Recover a length-indexed vector from a list. The length is not known statically, so it is packed existentially in a Sigma alongside the vector. The pair is built with the %[..] surface (which lowers to mk_pair while solving the dependent second-component motive from the expected Sigma type); a bare mk_pair(..) leaves that motive an unsolved metavariable.

  • # fn head(a: Type, n: Nat, xs: Vector(a, S(n))) -> a
  • # fn init(a: Type, n: Nat, xs: Vector(a, S(n))) -> Vector(a, n)

    All-but-the-last element of a non-empty vector, shrinking the length by one.

  • # fn is_empty(a: Type, n: Nat, xs: Vector(a, n)) -> Bool
  • # fn last(a: Type, n: Nat, xs: Vector(a, S(n))) -> a

    Last element of a non-empty vector. The S(n) index makes emptiness unrepresentable, so this is total with no Option.

  • # fn length(a: Type, n: Nat, xs: Vector(a, n)) -> Nat
  • # fn lookup(a: Type, n: Nat, xs: Vector(a, n), index: Bounded(n)) -> a
  • # fn map(a: Type, b: Type, n: Nat, xs: Vector(a, n), f: Function(a, b)) -> Vector(b, n)
  • # fn product(n: Nat, xs: Vector(Int, n)) -> Int

    Product of an Int vector of any length.

  • # fn replicate(a: Type, n: Nat, x: a) -> Vector(a, n)
  • # fn reverse(a: Type, n: Nat, xs: Vector(a, n)) -> Vector(a, n)

    Reverse the vector, preserving its length. Each prepend is turned into a snoc on the reversed tail, so the length is provably unchanged (Vector(a, n) -> Vector(a, n)) without any auxiliary plus-lemma.

  • # fn set(a: Type, n: Nat, xs: Vector(a, n), index: Bounded(n), value: a) -> Vector(a, n)
  • # fn singleton(a: Type, x: a) -> Vector(a, S(Z))
  • # fn snoc(a: Type, n: Nat, xs: Vector(a, n), y: a) -> Vector(a, S(n))

    Append one element at the END of the vector, growing the length by one. Total: the length index tracks the growth exactly, mirroring prepend at the other end. snoc is the workhorse behind reverse.

  • # fn sum(n: Nat, xs: Vector(Int, n)) -> Int

    Sum of an Int vector of any length.

  • # fn tail(a: Type, n: Nat, xs: Vector(a, S(n))) -> Vector(a, n)
  • # fn take(a: Type, n: Nat, m: Nat, xs: Vector(a, plus(n, m))) -> Vector(a, n)

    First n elements of a vector whose length is plus(n, m), dropping the trailing m. with n (not match n) is the Idris-style convoy: matching n refines the sibling xs : Vector(a, plus(n, m)) per branch, so in the S(k) branch xs : Vector(a, plus(S(k), m)) — a non-empty vector — and the inner match xs legitimately omits empty. That omission is discharged because coverage normalizes the scrutinee index: plus(S(k), m) reduces to S(plus(k, m)), whose S head refutes empty's Z.

  • # fn to_list(a: Type, n: Nat, xs: Vector(a, n)) -> List(a)

    Forget the length index, projecting to an ordinary List.

  • # fn update(a: Type, n: Nat, xs: Vector(a, n), index: Bounded(n), f: Function(a, a)) -> Vector(a, n)
  • # fn zip(a: Type, b: Type, n: Nat, xs: Vector(a, n), ys: Vector(b, n)) -> Vector(Tuple(a, b), n)

    Pair two equal-length vectors element-wise into a vector of 2-tuples.

  • # fn zip_with(a: Type, b: Type, c: Type, n: Nat, xs: Vector(a, n), ys: Vector(b, n), f: Function(a, Function(b, c))) -> Vector(c, n)