[Agda] Bug in simplification?

[Philip Wadler]

Thank you. Done! -- 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 18:02, Ulf Norell <ulf.norell at gmail.com> wrote:

> 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/20180318/205822d3/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180318/205822d3/attachment.ksh>