tutorial-code icon indicating copy to clipboard operation
tutorial-code copied to clipboard

`Mat m n` instead of `Mat n m`?

Open ShreckYe opened this issue 3 years ago • 1 comments

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?

ShreckYe avatar Jun 13 '21 11:06 ShreckYe

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.

ice1000 avatar Jun 14 '21 02:06 ice1000