1.4. Worked example
The block builds an integer matrix with the #m[...] literal and checks
three things about it: the squared norm of the first row
(2² + 0² + 1² = 5), the dot product of the first two rows (4), and
that the identity fixes a vector.
open Hex
namespace HexMatrixChapterExample
def A : Matrix Int 3 3 := #m[2, 0, 1; 1, 3, 2; 0, 1, 1]
#guard (A.row 0).normSq = 5
#guard (A.row 0).dotProduct (A.row 1) = 4
def v : Vector Int 3 := #v[1, 2, 3]
#guard (Matrix.identity (R := Int) 3).mulVec v = v
end HexMatrixChapterExample