English
Vector of length n from a function on Fin n: ofFn(n,f) yields a vector whose i-th coordinate is f(i). Defined by recursion: for n=0, nil; for n>0, cons (f 0) (ofFn (λ i, f i.succ)).
Русский
Вектор длины n из функции на Fin n: ofFn(n,f) образует вектор, где i-ая координата равна f(i). Определено по рекурсии: при n=0 — nil; при n>0 — cons (f 0) (ofFn (λ i, f i.succ)).
LaTeX
$$$\\text{ofFn} : \\forall n, (\\mathrm{Fin}\\,n \\to \\alpha) \\to \\text{Vector } \\alpha n\\quad\\text{соответствует}\\quad\\begin{cases} \\text{ofFn}(0,f)=\\text{nil}, \\\\ \\text{ofFn}(n+1,f)=\\text{cons}(f(0),\\ \\text{ofFn}(n,\\ \\lambda i. f(i.succ))).\\end{cases}$$$
Lean4
/-- Take `i` elements from a vector of length `n`; we can have `i > n`. -/
def take (i : ℕ) : Vector α n → Vector α (min i n)
| ⟨l, p⟩ => ⟨List.take i l, by simp [*]⟩
