From 2318ee7660c0cd0e002ed90ed1282dfb5d374c26 Mon Sep 17 00:00:00 2001 From: Kiana Sheibani Date: Fri, 26 Apr 2024 01:02:43 -0400 Subject: [PATCH] Fix use of removed function --- src/Data/NumIdr/Matrix.idr | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/NumIdr/Matrix.idr b/src/Data/NumIdr/Matrix.idr index 9f2c97f..e7943ab 100644 --- a/src/Data/NumIdr/Matrix.idr +++ b/src/Data/NumIdr/Matrix.idr @@ -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.