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