English
Vec is a predicate that says a vector-valued function is partial recursive for each coordinate: f : List.Vector ℕ n → List.Vector ℕ m is such that for every i, the i-th projection is Partrec'.
Русский
Vec — это предикат, указывающий, что векторнозначная функция частично вычислима для каждого координаты: для каждой i, (f v).get i — частично вычислима.
LaTeX
$$$$\mathrm{Vec}_{n,m}(f) := \forall i, \mathrm{Partrec'}(\lambda v. (f\;v).get\;i).$$$$
Lean4
/-- Analogous to `Nat.Partrec'` for `ℕ`-valued functions, a predicate for partial recursive
vector-valued functions. -/
def Vec {n m} (f : List.Vector ℕ n → List.Vector ℕ m) :=
∀ i, Partrec' fun v => (f v).get i
