[Agda] Strange bug

[Philip Wadler]

Excellent! Thank you, -- 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 Mon, 25 Feb 2019 at 08:47, Guillaume Allais <
guillaume.allais at ens-lyon.org> wrote:

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