[Agda] Strange bug

Philip Wadler wadler at inf.ed.ac.uk
Mon Feb 25 00:31:57 CET 2019


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/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190224/d756b3cc/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: CoercionsS.lagda
Type: application/octet-stream
Size: 2453 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190224/d756b3cc/attachment.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Types.agda
Type: application/octet-stream
Size: 19948 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190224/d756b3cc/attachment-0001.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Labels.agda
Type: application/octet-stream
Size: 204 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190224/d756b3cc/attachment-0002.obj>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190224/d756b3cc/attachment.ksh>


More information about the Agda mailing list