repeat — Mathlib

English

repeat n t is a TypeVec n consisting of n copies of the element t.

Русский

repeat n t — вектор длины n, содержащий n копий элемента t.

LaTeX

$$$$\\text{repeat}: \\mathbb{N} \\to (\\text{Sort} \\to \\text{TypeVec}n)$$$$

Lean4

/-- `repeat n t` is a `n-length` type vector that contains `n` occurrences of `t` -/
def «repeat» : ∀ (n : ℕ), Sort _ → TypeVec n
  | 0, _ => Fin2.elim0
  | Nat.succ i, t => append1 («repeat» i t) t

Похожие утверждения