English
The head of vecCons x u is x, and the tail is u.
Русский
Голова vecCons x u равна x, хвост — это u.
LaTeX
$$$\mathrm{vecHead}(\mathrm{vecCons} x u) = x\quad\text{and}\quad \mathrm{vecTail}(\mathrm{vecCons} x u) = u$$$
Lean4
/-- Parses a chain of `Matrix.vecCons` calls into elements, leaving everything else in the tail.
`let ⟨xs, tailn, tail⟩ ← matchVecConsPrefix n e` decomposes `e : Fin n → _` in the form
`vecCons x₀ <| ... <| vecCons xₙ <| tail` where `tail : Fin tailn → _`. -/
partial def matchVecConsPrefix (n : Q(Nat)) (e : Expr) : MetaM <| List Expr × Q(Nat) × Expr := do
match_expr ← Meta.whnfR e with
| Matrix.vecCons _ n x xs =>
do
let (elems, n', tail) ← matchVecConsPrefix n xs
return (x :: elems, n', tail)
| _ =>
return ([], n, e)
