A RetroSearch Logo

Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Search Query:

Showing content from https://github.com/agda/agda/issues/7084 below:

Mimer triggers __IMPOSSIBLE__ in my homework assignment · Issue #7084 · agda/agda · GitHub

Agda version 2.6.5-a445e3b

Error message:

An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full/Agda/TypeChecking/Telescope.hs:668:24 in Agda-2.6\
.5-inplace:Agda.TypeChecking.Telescope

https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/Telescope.hs#L668

For obvious reasons I can't share the reproduction publicly, but I can send a link to a private gist file to those who work on Mimer through emails.

EDIT: managed to simplify it by a LOT and does not contain my solutions:
https://gist.github.com/ice1000/0b0730d4b57d23ad974c060ef8a748f4


RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4