[Agda] Bug caused by new forcing translation

Ulf Norell ulf.norell at gmail.com
Mon Mar 5 09:02:15 CET 2018


You can revert to b8eb5098, which is when the code was added, but before it
was actually run.

/ Ulf

On Mon, Mar 5, 2018 at 8:23 AM, stvienna wiener <stvienna at gmail.com> wrote:

> Hi all,
>
> My formalization doesn't work because of the open bug:
> https://github.com/agda/agda/issues/2888
>
> (Location of the error: Forcing.hs:230)
>
>
> Is there a work around so that I can keep on working?
> What agda commit should I revert to? (I.e., in which commit was the
> new forcing translation introduced?)
>
> Best,
> Stephan
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180305/39eaa43f/attachment.html>


More information about the Agda mailing list