git.iko.soy/Idris-dev
on master help sign in
Merge pull request #803 from alexeevg/master
e0aa8a4Edwin Brady
libs/prelude/Prelude/Vect.idr+26
compare with master
unifiedsplit
@@ -99,6 +99,32 @@ unzip : Vect n (a, b) -> (Vect n a, Vect n b)
99unzip [] = ([], [])
99unzip [] = ([], [])
100unzip ((l, r)::xs) with (unzip xs)
100unzip ((l, r)::xs) with (unzip xs)
101 | (lefts, rights) = (l::lefts, r::rights)
101 | (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+
102
128
103--------------------------------------------------------------------------------
129--------------------------------------------------------------------------------
104-- Maps
130-- Maps