#m[...] literal notation and grid pretty-printing for Hex.Matrix.

#m[a, b; c, d] builds the matrix with rows [a, b] and [c, d]: rows are separated by ; and entries by ,, mirroring Mathlib's !![...] but with a distinct opening token, so the two notations coexist in the Mathlib bridge libraries (Mathlib owns ![ and !![).

#m[1, 2;
   3, 4]   -- : Hex.Matrix Int 2 2

A literal collects its rows into nested #v[...] vectors and feeds them to Hex.Matrix.ofFn, so the construction goes through the public matrix API. Row lengths are checked by the elaborator: a ragged literal fails to typecheck rather than silently building a malformed matrix.

The Repr instance renders a matrix back in #m[...] notation under #eval, column-aligned and copy-pasteable as input.

def Hex.Matrix.matrixLiteral : Lean.ParserDescr

#m[a, b; c, d] is the Hex.Matrix with rows [a, b] and [c, d]. Rows are ;-separated and entries ,-separated.

Equations

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

def Hex.Matrix.render {R : Type u_1} {n m : Nat} [Repr R] (M : Matrix R n m) : Std.Format

Render M in #m[...] notation, with entries right-justified per column so the columns line up. The output is copy-pasteable as input. For example,

#m[ 0, 2,  1;
   -6, 0, -8;
    5, 6,  0]

This is what the Repr instance shows under #eval.

Equations

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

@[implicit_reducible, instance 10000]

instance Hex.Matrix.instRepr {R : Type u_1} {n m : Nat} [Repr R] : Repr (Matrix R n m)

Show matrices in copy-pasteable #m[...] notation under #eval/Repr. Higher priority than the #v[...] vector instance below so a matrix renders as a grid rather than as a nested vector of vectors.

Equations

• Hex.Matrix.instRepr = { reprPrec := fun (M : Hex.Matrix R n m) (x : Nat) => M.render }

@[implicit_reducible]

instance Hex.Matrix.instToStringOfRepr {R : Type u_1} {n m : Nat} [Repr R] : ToString (Matrix R n m)

The #m[...] rendering as a String.

Equations

• Hex.Matrix.instToStringOfRepr = { toString := fun (M : Hex.Matrix R n m) => M.render.pretty }

@[implicit_reducible, instance 10000]

instance Hex.Matrix.reprVector {R : Type u_1} {n : Nat} [Repr R] : Repr (Vector R n)

Render a vector in copy-pasteable #v[...] notation under #eval/Repr, mirroring the #m[...] matrix rendering. Higher priority than the core deriving Repr instance, so a bare vector (for example a matrix row or an LLL short vector) prints as #v[...] and can be pasted straight back as input.

Equations

• Hex.Matrix.reprVector = { reprPrec := fun (v : Vector R n) (x : Nat) => Std.Format.text ("#v[" ++ ", ".intercalate (List.map (fun (x : R) => (repr x).pretty) v.toList) ++ "]") }