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