[Agda] Bug in simplification?

[Philip Wadler]

Thanks, that works! My final solution is attached.

The '1' that appears in printing the function body in my original message
appears to be a bug, and should be fixed. If it's not on a list of known
bugs, what would I do to add it?

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/

On 17 March 2018 at 15:22, András Kovács <kovacsahun at hotmail.com> wrote:

> 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/1ea5f93e/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: DecidableFixed.agda
Type: application/octet-stream
Size: 806 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180317/1ea5f93e/attachment.obj>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180317/1ea5f93e/attachment.ksh>