Lean4
@[macro Matrix.matrixNotation]
public meta def _aux_Mathlib_LinearAlgebra_Matrix_Notation___macroRules_Matrix_matrixNotation_1 : Macro✝ := fun
| `(!![$[$[$rows],*];*]) => do
let m := rows.size
let n := if h : 0 < m then rows[0].size else 0
let rowVecs ←
rows.mapM fun row : Array Term => do
unless row.size = n do
Macro.throwErrorAt (mkNullNode row)
s! "\
Rows must be of equal length; this row has {row.size } items, \
the previous rows have {n}"
`(![$row,*])
`(@Matrix.of (Fin $(quote m)) (Fin $(quote n)) _ ![$rowVecs,*])
| _ => no_error_if_unused% throw✝ Lean.Macro.Exception.unsupportedSyntax✝
