on master help sign in
Use new syntax in lib
commitc8b0f28b31c2fb2f608c970be06dda03d6c3dcb0 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 6 Jan 2012, 16:54 (15 years ago) parentf7c50cf
3 files changed+11−11
lib/prelude/list.idr+7−6 lib/prelude/vect.idr+3−4 tutorial/classes.tex+1−1
lib/prelude/list.idr+7−6
@@ -65,8 +65,8 @@ lookup k ((x, v) :: xs) = if (x == k) then (Just v) else (lookup k xs);
6565sort : Ord a => List a -> List a;
6666sort [] = [];
6767sort [x] = [x];
68−sort xs = let s = split xs in
69− merge (sort (fst s)) (sort (snd s)) where {
68+sort xs = let (x, y) = split xs in
69+ merge (sort x) (sort y) where {
7070 splitrec : List a -> List a -> (List a -> List a) -> (List a, List a);
7171 splitrec (_ :: _ :: xs) (y :: ys) zs = splitrec xs ys (zs . ((::) y));
7272 splitrec _ ys zs = (zs [], ys);
@@ -95,7 +95,8 @@ break p = span (not . p);
9595
9696split : (a -> Bool) -> List a -> List (List a);
9797split p [] = [];
98−split p xs with break p xs {
99− | (chunk, []) = [chunk];
100− | (chunk, (c :: rest)) = chunk :: split p rest;
101−}
98+split p xs = case break p xs of {
99+ (chunk, []) => [chunk]
100+ | (chunk, (c :: rest)) => chunk :: split p rest
101+ };
102+
lib/prelude/vect.idr+3−4
@@ -32,10 +32,9 @@ app (x :: xs) ys = x :: app xs ys;
3232
3333filter : (a -> Bool) -> Vect a n -> (p ** Vect a p);
3434filter p [] = ( _ ** [] );
35−filter p (x :: xs) with filter p xs {
36− | ( _ ** xs' )
37− = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' );
38−}
35+filter p (x :: xs)
36+ = let (_ ** xs') = filter p xs in
37+ if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' );
3938
4039map : (a -> b) -> Vect a n -> Vect b n;
4140map f [] = [];
tutorial/classes.tex+1−1
@@ -299,7 +299,7 @@ the following function:
299299
300300\begin{SaveVerbatim}{guardq}
301301
302−guard : MonadPlus m => Bool -> m ()
302+guard : MonadPlus m => Bool -> m ();
303303
304304\end{SaveVerbatim}
305305\useverb{guardq}