| inductive Vector' (α : Type u) : Nat → Type u | |
| | nil : Vector' α 0 | |
| | cons : α → Vector' α n → Vector' α (n+1) | |
| deriving Repr | |
| infix:67 " :: " => Vector'.cons | |
| def tabulate (f : Fin n → α) : Vector' α n := | |
| match n with | |
| | 0 => Vector'.nil | |
| | n+1 => f 0 :: tabulate (f ∘ Fin.succ) | |
| #eval tabulate fun i : Fin 5 => i |