@@ -58,6 +58,17 @@ extraneous and may be omitted:
58 filter p (x :: xs) with (filter p xs)
58 filter p (x :: xs) with (filter p xs)
59 | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
59 | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
61+``with`` clauses can also be nested:
65+ foo : Int -> Int -> Bool
66+ foo n m with (succ n)
67+ foo _ m | 2 with (succ m)
68+ foo _ _ | 2 | 3 = True
69+ foo _ _ | 2 | _ = False
61If the intermediate computation itself has a dependent type, then the
72If the intermediate computation itself has a dependent type, then the
62result can affect the forms of other arguments — we can learn the form
73result can affect the forms of other arguments — we can learn the form
63of one value by testing another. In these cases, view refined argument
74of one value by testing another. In these cases, view refined argument