git.iko.soy/Idris-dev
on master help sign in
Update Matrix.idr
9d26777Cliff Harvey
libs/base/Data/Matrix.idr+33−14
compare with master
unifiedsplit
@@ -1,6 +1,7 @@
1module Data.Matrix
1module Data.Matrix
2
2
3import Data.Complex
3import Data.Complex
4+import Data.ZZ
4
5
5%default total
6%default total
6
7
@@ -215,7 +216,39 @@ instance Ring Float where
215
216
216instance RingWithUnity Float where
217instance RingWithUnity Float where
217 unity = 1
218 unity = 1
219+
220+
221+instance Semigroup Nat where
222+ (<+>) = (+)
223+
224+instance Monoid Nat where
225+ neutral = 0
218
226
227+instance VerifiedSemigroup Nat where
228+ semigroupOpIsAssociative = plusAssociative
229+
230+instance VerifiedMonoid Nat where
231+ monoidNeutralIsNeutralL = plusZeroRightNeutral
232+ monoidNeutralIsNeutralR = plusZeroLeftNeutral
233+
234+
235+instance Semigroup ZZ where
236+ (<+>) = (+)
237+
238+instance Monoid ZZ where
239+ neutral = 0
240+
241+instance Group ZZ where
242+ inverse = (* -1)
243+
244+instance AbelianGroup ZZ
245+
246+instance Ring ZZ where
247+ (<*>) = (*)
248+
249+instance RingWithUnity ZZ where
250+ unity = 1
251+
219
252
220instance Semigroup a => Semigroup (Complex a) where
253instance Semigroup a => Semigroup (Complex a) where
221 (<+>) (a :+ b) (c :+ d) = (a <+> c) :+ (b <+> d)
254 (<+>) (a :+ b) (c :+ d) = (a <+> c) :+ (b <+> d)
@@ -233,17 +266,3 @@ instance (Num a, AbelianGroup (Complex a)) => Ring (Complex a) where
233
266
234instance (Num a, Ring (Complex a)) => RingWithUnity (Complex a) where
267instance (Num a, Ring (Complex a)) => RingWithUnity (Complex a) where
235 unity = (1 :+ 0)
268 unity = (1 :+ 0)
236−
237−
238−instance Semigroup Nat where
239− (<+>) = (+)
240−
241−instance Monoid Nat where
242− neutral = 0
243−
244−instance VerifiedSemigroup Nat where
245− semigroupOpIsAssociative = plusAssociative
246−
247−instance VerifiedMonoid Nat where
248− monoidNeutralIsNeutralL = plusZeroRightNeutral
249− monoidNeutralIsNeutralR = plusZeroLeftNeutral