[Agda] Nested with

[andy morris]

2009/6/5 Ben Horsfall <ben.horsfall at gmail.com>:
> Could someone post/direct me to an example of a nested with-expression?
>
>
> Ben
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

Contrived, I know, but I couldn't think of a better example off the
top of my head :)

both-zero : ℕ → ℕ → Bool
both-zero x y with x | y
... | zero | zero = true
... | _    | _    = false