English
The function res(x,n) returns the list of the first n entries of x, with res x 0 = nil and res x (n+1) = x n :: res x n.
Русский
Функция res(x,n) возвращает список первых n элементов x, причём res x 0 = пустой список, а res x (n+1) = x(n) :: res x n.
LaTeX
$$$res(x,0)=[]$, and $res(x,n+1)=x(n) :: res(x,n)$$$
Lean4
/-- In the case where `E` has constant value `α`,
the cylinder `cylinder x n` can be identified with the element of `List α`
consisting of the first `n` entries of `x`. See `cylinder_eq_res`.
We call this list `res x n`, the restriction of `x` to `n`. -/
def res (x : ℕ → α) : ℕ → List α
| 0 => nil
| Nat.succ n => x n :: res x n
