[Agda] Bug in simplification?

[András Kovács]

Hi,

As far as I know, the issue is that

1. Agda elaborates pattern matching lambdas to new top-level definitions
with machine-generated names
2. Agda does not look into bodies of pattern matching functions when
checking definitional equality

Hence, Agda doesn't know that two pattern matching lambdas which look the
same in the source are equal.

People tolerate this limitation because we rarely rely on the rather
fragile intensional equality of functions. Instead we postulate function
extensionality when required.

If you'd like to have a bit more intensional function equality, you can use
top-level lemmas instead of pattern lambdas, like this
<http://lpaste.net/363727>.

If you'd like to have as much as possible intensional function equality,
you need to write all of your functions in terms of eliminators, thereby
making all of your function bodies visible to Agda, as induction method
arguments to eliminators.

2018-03-17 18:59 GMT+01:00 Philip Wadler <wadler at inf.ed.ac.uk>:

> Why does the attached not work? Is there a workaround, or a repair on the
> horizon? Note particularly the "1" in the error message, which appears
> spurious. Cheers, -- P
>
> .   \ Philip Wadler, Professor of Theoretical Computer Science,
> .   /\ School of Informatics, University of Edinburgh
> .  /  \ and Senior Research Fellow, IOHK
> . http://homepages.inf.ed.ac.uk/wadler/
>
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180317/c9eea15c/attachment.html>