English
There is a canonical encoding that associates each finite m×n matrix with entries in α to a quoted representation of that matrix; the encoding mkLiteralQ maps a matrix to its quoted form.
Русский
Существует каноничeскeе кодирование для конечной матрицы размером m×n с элементами α в символьную (quoted) форму; отображение mkLiteralQ переводит матрицу в её закодированное представление.
LaTeX
$$$\\text{mkLiteralQ}(A) = q\\bigl(\\mathrm{Matrix.of}(\\text{elems}(A))\\bigr) \\quad\\text{for } A \\in \\mathrm{Mat}_{m,n}(\\alpha)$$$
Lean4
/-- `Matrix.mkLiteralQ !![a, b; c, d]` produces the term `q(!![$a, $b; $c, $d])`. -/
def mkLiteralQ {u : Level} {α : Q(Type u)} {m n : Nat} (elems : Matrix (Fin m) (Fin n) Q($α)) :
Q(Matrix (Fin $m) (Fin $n) $α) :=
let elems := PiFin.mkLiteralQ (α := q(Fin $n → $α)) fun i => PiFin.mkLiteralQ fun j => elems i j
q(Matrix.of $elems)
