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