on master help sign in
Merge pull request #803 from alexeevg/master

Eq and Ord instances for Prelude.Vect

commite0aa8a429d7ff27c4d2c5e7e9328f99e50275258 authorEdwin Brady <edwin.brady@gmail.com> dateTue 28 Jan 2014, 05:32 (13 years ago) parente63fcefb837e4b
1 file changed+26
libs/prelude/Prelude/Vect.idr+26
libs/prelude/Prelude/Vect.idr+26
@@ -99,6 +99,32 @@ unzip : Vect n (a, b) -> (Vect n a, Vect n b)
9999unzip [] = ([], [])
100100unzip ((l, r)::xs) with (unzip xs)
101101 | (lefts, rights) = (l::lefts, r::rights)
102+
103+--------------------------------------------------------------------------------
104+-- Equality
105+--------------------------------------------------------------------------------
106+
107+instance (Eq a) => Eq (Vect n a) where
108+ (==) [] [] = True
109+ (==) (x::xs) (y::ys) =
110+ if x == y then
111+ xs == ys
112+ else
113+ False
114+
115+
116+--------------------------------------------------------------------------------
117+-- Order
118+--------------------------------------------------------------------------------
119+
120+instance Ord a => Ord (Vect n a) where
121+ compare [] [] = EQ
122+ compare (x::xs) (y::ys) =
123+ if x /= y then
124+ compare x y
125+ else
126+ compare xs ys
127+
102128
103129--------------------------------------------------------------------------------
104130-- Maps