[Agda] Nested with

[Andrés Sicard-Ramírez]

Hi Ben,

On Thu, Jun 4, 2009 at 8:09 PM, Ben Horsfall<ben.horsfall at gmail.com> wrote:
> Could someone post/direct me to an example of a nested with-expression?

I know the examples are too much trivial, but I hope they help

open import Data.Bool
open import Data.Nat

areTrueAndZero : Bool -> ℕ -> Bool
areTrueAndZero b n with b
... | false = false
... | true with n
...   | zero = true
...   | _    = false

areTrueAndZero' : Bool -> ℕ -> Bool
areTrueAndZero' b n with b
areTrueAndZero' b n | false = false
areTrueAndZero' b n | true with n
areTrueAndZero' b n | true | zero = true
areTrueAndZero' b n | true | _    = false

areTrueAndZero'' : Bool -> ℕ -> Bool
areTrueAndZero'' b n with b | n
... | true  | zero = true
... | _     | _    = false


Moreover, I found an example (the function 'all') in
Agda/examples/SummerSchool07/Solutions/Problems4.agda

Best,

-- 
Andrés