[Agda] Bug in simplification?

[Ulf Norell]

You can report it by clicking the "New Issue" button here:
https://github.com/agda/agda/issues

/ Ulf

On Sat, Mar 17, 2018 at 9:28 PM, Philip Wadler <wadler at inf.ed.ac.uk> wrote:

> 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
>>>
>>>
>>
>
> 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/ac79fbab/attachment.html>