[Agda] difficulties with patterns

[Nils Anders Danielsson]

On 2013-11-28 18:05, Sergei Meshveliani wrote:
> I tried to compose a stand-alone example of 5 - 15 lines, but my first
> simple attempt has failed.
>
> If you do not see such an example, I could consider reducing the
> existing one.

I haven't studied your example, but I guess that your problem is related
to the following example, in which the code is rejected because x can't
be unified with y:

   Rejected : (x y : ℕ) → x ≡ y → Set₁
   Rejected x y eq = case eq of λ
     { refl → Set }

An awkward workaround:

   Accepted : (x y : ℕ) → x ≡ y → Set₁
   Accepted x y eq = case (∃₂ λ x y → x ≡ y) ∋ (x , y , eq) of λ
     { (z , .z , refl) → Set }

-- 
/NAD