Parsing matrix literals

Parsers matching !![…] matrix literal expressions into their dimensions, element type, and entry expressions, for tactics evaluating functions of a concrete matrix.

TODO: !![…] still elaborates to Matrix.of applied to Matrix.vecCons chains; but there is a wip draft PR that switches it to the merged Matrix.ofArray.

This files needs a corresponding adaptation if that is merged -- but in the best case, the entirety of this file can be gone.

Main definitions

• matchMatrixLit?: match a closed matrix literal.

def Mathlib.Tactic.Echelon.matchMatrixLit? (A : Lean.Expr) : Lean.MetaM (Option (ℕ × ℕ × Lean.Expr × Array (Array Lean.Expr)))

Match a closed Fin-indexed matrix literal: its dimensions, element type, and rows of entries.

Equations

• One or more equations did not get rendered due to their size.