[Agda] Strange bug

[Pierre Lescanne]

I got the same bug, with 2.6.1.

But restarting agda, I fix it.

Perhaps I did not install Agda in an orthodox way !

Cheers,

Pierre

Le 25/02/2019 à 12:45, Guillaume Allais a écrit :
> Hi Phil,
>
> This particularly annoying bug has been fixed in 2.5.4.2:
> https://github.com/agda/agda/issues/3199
>
> Cheers,
> --
> gallais
>
> On 25/02/2019 00:31, Philip Wadler wrote:
>> I am getting a strange bug.
>>
>> An internal error has occurred. Please report this as a bug.
>>> Location of the error:
>>> src/full/Agda/TypeChecking/Serialise/Instances/Common.hs:178
>>
>> Relevant source files attached. The error occurs in CoercionsS.lagda.
>>
>> What is the best way to report this, please?   -- 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
>>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-- 
Cordialement,

---------------------------
Pierre Lescanne (Professeur émérite)
LIP / ENS de Lyon
46 allée d'Italie
69364 LYON Cedex 07, France
tél: +33 6 85 70 94 31
http://perso.ens-lyon.fr/pierre.lescanne/
---------------------------

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200612/392d3e5e/attachment.html>