[Agda] case ((a , b) , (c , d))

[Nils Anders Danielsson]

On 2013-11-11 14:51, Sergei Meshveliani wrote:
> Please, what is wrong here?

> f : ℕ → ℕ
> f n = case (  (n , suc n)  ,  (suc n , suc (suc n))  )
>        of \
>        { ( (zero , zero) , _             ) →  zero
>        ; ( _             , (zero , zero) ) →  zero
>        }

If you test the following code, then you can see that Agda doesn't infer
all of the implicit arguments in your case scrutinee:

   f : ℕ → ℕ
   f n = case (  (n , suc n)  ,  (suc n , suc (suc n))  )
         of ?

The most recent development version of Agda highlights unsolved
meta-variables and errors at the same time; perhaps this will make it
easier to understand errors caused by unsolved meta-variables.

You can fix your code by replacing some of the commas with _,′_:

   f n = case (  (n , suc n)  ,′  (suc n ,′ suc (suc n))  )
         of ?

-- 
/NAD