A RetroSearch Logo

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

Search Query:

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

parameter overflow in `declareData` · Issue #7576 · agda/agda · GitHub

open import Common.Reflection

unquoteDecl data D =
  declareData D 1 (quoteTerm Set)
An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at
src/full/Agda/TypeChecking/Unquote.hs:1162:25 in
Agda-2.8.0-Jy3QZyfEPpVKHSr0q4RiRx:Agda.TypeChecking.Unquote

There is also another impossible error at

open import Common.Reflection

unquoteDecl data D =
  declareData D 0 (quoteTerm Set)
An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at
src/full/Agda/TypeChecking/Serialise/Instances/Internal.hs:432:59
in
Agda-2.8.0-Jy3QZyfEPpVKHSr0q4RiRx:Agda.TypeChecking.Serialise.Instances.Internal

which appears to be unrelated.


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