Exhaustively define matrix / function

Stream: new members

[Shi Zhengyu]

Dear all,

I am not sure if this is the right way to put it, but what is the best way to define a matrix by explicitly writing out its contents? Or, since finite matrix is just a bivariate function (fin u) -> (fin v) -> \N, how do I define a function with finite domain by exhausting its range?

i.e. I am looking for notations like def A: FinMat := [[1, 0, 0], [0, 1, 0], [0, 0, 1]] for a matrix ...

Many Thanks!

[Heather Macbeth]

![![1, 0, 0], ![0, 1, 0], ![0, 0, 1]]

[Heather Macbeth]

After first

import data.matrix.notation

[Heather Macbeth]

You nearly guessed it! :)

[Shi Zhengyu]

Thanks! :D