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: !![…] elaborates to Matrix.of applied to Matrix.vecCons chains, which is the shape matched here. Once it elaborates through Matrix.ofArray instead, adapt this parser, or remove it if the array form can be read directly.

Main definitions

• matchMatrixLit?: match a matrix literal, closed by default.

def Mathlib.Tactic.Matrix.matchMatrixLit? (A : Lean.Expr) (closed : Bool := true) : Lean.MetaM (Option (ℕ × ℕ × Lean.Expr × Array (Array Lean.Expr)))

Match a Fin-indexed matrix literal: its dimensions, element type, and rows of entries; with closed := true, only a literal without free variables or metavariables.

Equations

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