@@ -58,6 +58,17 @@ extraneous and may be omitted:
5858 filter p (x :: xs) with (filter p xs)
5959 | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
6060
61+``with`` clauses can also be nested:
62+
63+.. code-block:: idris
64+
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
70+ foo _ _ | _ = False
71+
6172If the intermediate computation itself has a dependent type, then the
6273result can affect the forms of other arguments — we can learn the form
6374of one value by testing another. In these cases, view refined argument