tutorial-code
tutorial-code copied to clipboard
`Mat m n` instead of `Mat n m`?
By convention, in saying an m × n matrix the m comes before the n, where m denotes the number of rows and n denotes the number of columns.
In PartI/src/Exercises/IndexedEx.ard the matrix is defined as \func Mat (A : \Type) (n m : Nat) : \Type
and used as Mat n m
. Would it better to change it to \func Mat (A : \Type) (m n : Nat) : \Type
and Mat m n
?
Do you want to make a pull request? I guess we used this order since n
and m
on the keyboard appear to be in this order, but I'm not sure. Maybe @part-xx knows better than me.