| inductive Vector' (α : Type u) : Nat → Type u | |
| | nil : Vector' α 0 | |
| | cons : α → Vector' α n → Vector' α (n + 1) | |
| def test [Monad m] (xs : Vector' α a) : m Unit := | |
| match xs with | |
| | Vector'.nil => return () | |
| | Vector'.cons _ xs => test xs | |
| termination_by sizeOf xs |