git.iko.soy/Idris-dev
on master help sign in
Merge pull request #5 from IreneKnapp/master

Wrote a trivial .gitignore for you :)

commit32ab3b1741320ca9b5491b65367f5fc0732c0135 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateWed 25 Jan 2012, 13:58 (15 years ago) parentfc6eb5317cbae5
4 files changed+41−3
compare with master
unifiedsplit
.gitignore+2 lib/builtins.idr+11 lib/prelude.idr−3 lib/prelude/list.idr+28
.gitignorenew file+2
@@ -0,0 +1,2 @@
1+dist
2+*.ibc
lib/builtins.idr+11
@@ -113,6 +113,10 @@ instance Eq Char where
113113instance Eq String where
114114 (==) = boolOp prim__eqString
115115
116+instance (Eq a, Eq b) => Eq (a, b) where
117+ (==) (a, c) (b, d) = (a == b) && (c == d)
118+
119+
116120data Ordering = LT | EQ | GT
117121
118122class Eq a => Ord a where
@@ -172,6 +176,13 @@ instance Ord String where
172176 GT
173177
174178
179+instance (Ord a, Ord b) => Ord (a, b) where
180+ compare (xl, xr) (yl, yr) =
181+ if xl /= yl
182+ then compare xl yl
183+ else compare xr yr
184+
185+
175186class (Eq a, Ord a) => Num a where
176187 (+) : a -> a -> a
177188 (-) : a -> a -> a
lib/prelude.idr−3
@@ -165,9 +165,6 @@ syntax "[" [start] "," [next] ".." [end] "]"
165165
166166---- More utilities
167167
168−flip : (a -> b -> c) -> b -> a -> c
169−flip f x y = f y x
170−
171168sum : Num a => List a -> a
172169sum = foldl (+) 0
173170
lib/prelude/list.idr+28
@@ -110,6 +110,13 @@ split p xs = case break p xs of
110110 (chunk, []) => [chunk]
111111 (chunk, (c :: rest)) => chunk :: split p rest
112112
113+any : (a -> Bool) -> List a -> Bool
114+any predicate [] = False
115+any predicate (a::rest) =
116+ if predicate a
117+ then True
118+ else any predicate rest
119+
113120--------------------------------------------------------------------------------
114121-- Conversions
115122--------------------------------------------------------------------------------
@@ -133,3 +140,24 @@ catMaybes (x::xs) =
133140 Nothing => catMaybes xs
134141 Just j => j :: catMaybes xs
135142
143+--------------------------------------------------------------------------------
144+-- Instances
145+--------------------------------------------------------------------------------
146+
147+instance (Eq a) => Eq (List a) where
148+ (==) [] [] = True
149+ (==) (a::restA) (b::restB) =
150+ if a == b
151+ then restA == restB
152+ else False
153+ (==) _ _ = False
154+
155+
156+instance Ord a => Ord (List a) where
157+ compare [] [] = EQ
158+ compare [] _ = LT
159+ compare _ [] = GT
160+ compare (a::restA) (b::restB) =
161+ if a /= b
162+ then compare a b
163+ else compare restA restB