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

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

Internal error in opaque block when case splitting when just given extended lambda · Issue #7218 · agda/agda · GitHub

For the code below, the following sequence of commands produces an internal error on version 2.6.4 and on master:

1. Refine the goal with λ { x → {! x !} }
2. Case-split on x

data ⊤ : Set where
  tt : ⊤

opaque
  f : ⊤ → ⊤
  f = {! λ { x → {! x !} } !}

The error is

An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full\Agda\Interaction\MakeCase.hs:222:7 in Agda-2.6.5-2CGFfl0UVRq2oEiF8zwYoq:Agda.Interaction.MakeCase

Reloading between refining and case-splitting does not give an error.

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