tutorial-code
tutorial-code copied to clipboard
`Mat m n` instead of `Mat n m`?
trafficstars
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.