c8b0f28 · Idris-dev · git.iko.soy

lib/prelude/list.idr+7−6

compare with master

unifiedsplit

@@ -65,8 +65,8 @@ lookup k ((x, v) :: xs) = if (x == k) then (Just v) else (lookup k xs);

65sort : Ord a => List a -> List a;

66sort [] = [];

67sort [x] = [x];

68−sort xs = let s = split xs in

68+sort xs = let (x, y) = split xs in

69− merge (sort (fst s)) (sort (snd s)) where {

69+ merge (sort x) (sort y) where {

70 splitrec : List a -> List a -> (List a -> List a) -> (List a, List a);

71 splitrec (_ :: _ :: xs) (y :: ys) zs = splitrec xs ys (zs . ((::) y));

72 splitrec _ ys zs = (zs [], ys);

@@ -95,7 +95,8 @@ break p = span (not . p);

95

96split : (a -> Bool) -> List a -> List (List a);

97split p [] = [];

98−split p xs with break p xs {

98+split p xs = case break p xs of {

99− | (chunk, []) = [chunk];

99+ (chunk, []) => [chunk]

100− | (chunk, (c :: rest)) = chunk :: split p rest;

100+ | (chunk, (c :: rest)) => chunk :: split p rest

101−}

101+ };

102+

lib/prelude/vect.idr+3−4

@@ -32,10 +32,9 @@ app (x :: xs) ys = x :: app xs ys;

32

33filter : (a -> Bool) -> Vect a n -> (p ** Vect a p);

34filter p [] = ( _ ** [] );

35−filter p (x :: xs) with filter p xs {

35+filter p (x :: xs)

36− | ( _ ** xs' )

36+ = let (_ ** xs') = filter p xs in

37− = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' );

37+ if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' );

38−}

39

38

40map : (a -> b) -> Vect a n -> Vect b n;

39map : (a -> b) -> Vect a n -> Vect b n;

41map f [] = [];

40map f [] = [];

tutorial/classes.tex+1−1

@@ -299,7 +299,7 @@ the following function:

299

300\begin{SaveVerbatim}{guardq}

301

302−guard : MonadPlus m => Bool -> m ()

302+guard : MonadPlus m => Bool -> m ();

303

304\end{SaveVerbatim}

305\useverb{guardq}