Fix use of removed function

This commit is contained in:
Kiana Sheibani 2024-04-26 01:02:43 -04:00
parent 762a41c32b
commit 2318ee7660
Signed by: toki
GPG key ID: 6CB106C25E86A9F7

View file

@ -33,7 +33,7 @@ Matrix' n = Array [n,n]
export
matrix : {default B rep : Rep} -> RepConstraint rep a => {m, n : _} ->
Vect m (Vect n a) -> Matrix m n a
matrix x = array' {rep} [m,n] x
matrix x = array {rep, s=[m,n]} x
||| Construct a matrix with a specific value along the diagonal.