Version-2-1-2

This version introduces the ... syntax for with clauses:

 filter : {A : Set} -> (A -> Bool) -> List A -> List A
 filter p [] = []
 filter p (x :: xs) with p x
 ...                | true  = x :: filter p xs
 ...                | false = filter p xs

is now equivalent to

 filter : {A : Set} -> (A -> Bool) -> List A -> List A
 filter p [] = []
 filter p (x :: xs) with p x
 filter p (x :: xs) | true  = x :: filter p xs
 filter p (x :: xs) | false = filter p xs
Page last modified on August 16, 2007, at 02:56 pm
Powered by PmWiki