From da4bb5873cefc92600c337dfd91d5194fbe07b57 Mon Sep 17 00:00:00 2001 From: Kiana Sheibani Date: Fri, 2 Sep 2022 21:45:10 -0400 Subject: [PATCH] Make small adjustments to code --- src/Data/NumIdr/Matrix.idr | 2 +- src/Data/NumIdr/Multiply.idr | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Data/NumIdr/Matrix.idr b/src/Data/NumIdr/Matrix.idr index 8e89120..75f7e61 100644 --- a/src/Data/NumIdr/Matrix.idr +++ b/src/Data/NumIdr/Matrix.idr @@ -350,7 +350,7 @@ detWithLUP : (Ord a, Abs a, Neg a, Fractional a) => (mat : Matrix' n a) -> DecompLUP mat -> a detWithLUP {n} mat lup = (if numSwaps lup `mod` 2 == 0 then 1 else -1) - * product (diagonal lup.lower) * product (diagonal lup.upper) + * product (diagonal lup.lu) export det : (Ord a, Abs a, Neg a, Fractional a) => Matrix' n a -> a diff --git a/src/Data/NumIdr/Multiply.idr b/src/Data/NumIdr/Multiply.idr index 6772716..6c0f062 100644 --- a/src/Data/NumIdr/Multiply.idr +++ b/src/Data/NumIdr/Multiply.idr @@ -56,7 +56,7 @@ namespace Monoid ||| Raise a multiplicative value (e.g. a matrix or a transformation) to a natural ||| number power. public export -power : MultGroup a => Nat -> a -> a +power : MultMonoid a => Nat -> a -> a power 0 _ = identity power 1 x = x power (S n@(S _)) x = x *. power n x @@ -66,5 +66,5 @@ power (S n@(S _)) x = x *. power n x ||| ||| This is the operator form of `power`. public export %inline -(^) : MultGroup a => a -> Nat -> a +(^) : MultMonoid a => a -> Nat -> a a ^ n = power n a