You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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?
The text was updated successfully, but these errors were encountered:
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.
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 asMat n m
. Would it better to change it to\func Mat (A : \Type) (m n : Nat) : \Type
andMat m n
?The text was updated successfully, but these errors were encountered: