[Agda] I'm not sure... case for the constructor ..., because I get stuck when trying to solve...

[Dmytro Starosud]

Hello guys,

I am trying to write a function on indexed types:
https://gist.github.com/dima-starosud/7100947b0e243ea6a034
But I cannot understand the reason of the error messages shown, and how to
solve issues arisen.

Please see a gist (link above).
Ideally I wanted "reduce₁". But that didn't compile. (And I think I can
imagine the reason why)

Next attempt was "reduce₂". But this would involve a lot of unnecessary
code on RHSs.

Than I decided to improve it and got "reduce₃", but it gave me completely
puzzling error message.

Please help me to understand all that stuff Agda communicates to me.

I would like something really simple (like "reduce₁"), probably with help
of *pattern*s.

Thanks in advance,
Dmytro
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20141205/065e3284/attachment.html