[Agda] Stranga konduto !

[G. Allais]

Hi Serge,

During the last Agda meeting, Jesper spent some time expanding
the documentation and he added a paragraph explaining why you
may encounter these sort of issues:

http://agda.readthedocs.io/en/latest/language/function-definitions.html#case-trees

He has also done work towards having overlapping, order-independent
patterns but I don't think any of this has landed in Agda (and don't
know of any plans to integrate this work in the near future).

https://lirias.kuleuven.be/handle/123456789/442509

So for the moment you'll have to keep proving the equation by pattern
matching (or reorder the patterns if you have a preferred reduction
behaviour).

Cheers,

gallais

On 09/05/16 12:48, Serge Leblanc wrote:
> Kial mi bezonas kazstudadon ĉe 'x' kvankam mi antaŭe indikis la egalecon
> 'diag x (suc y) = suc (diag (suc x) y)'?
> Plie, la erara mesago kontraŭdiras mian difinon de 'diag x (suc y)'?
>
> Why I need a case study on 'x' though I have previously pointed out the
> equality of 'diag x (suc y) = suc (diag (suc x), y)'?
> Moreover, the error message contradicts my definition of 'diag x (suc y)'?
>
>
> /home/serge/agda/Test.agda:12,13-17
> diag x (suc y) != suc (diag (suc x) y) of type ℕ
> when checking that the expression refl has type
> diag x (suc y) ≡ suc (diag (suc x) y)
>
>
> Sincere,
> --
> Serge Leblanc
> ------------------------------------------------------------------------
> gpg --keyserver hkp://keyserver.ubuntu.com:11371 --recv-keys 0x67B17A3F
> Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>