I apologize in advance if this is a duplicate issue - I'm not entirely sure what the problem is, so I can't be sure.
Error text:
An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full/Agda/Interaction/MakeCase.hs:156:42 in Agda-2.7.0.1-5961dbb805b69510352423fbb7020b1fac6732185b8b7f0d901cd2615432cabe:Agda.Interaction.MakeCase
Reproduction steps:
Navigate to hole on last line
subst-shift-pres {Γ} {V x} {sub} {ty₁} {ty₂} ⊢tm with compare x 1 in eq
... | k = {!!}
With Emacs' Agda Mode, perform a case split on eq with C-c C-c. Reproduces on my machine, and produces the above text.
I have tried to minimize the file as much as I can while retaining the error. (Apologies for the long copy paste; I can't upload an Agda file apparently)
import Relation.Binary.PropositionalEquality as Eq
open import Data.Nat using (ℕ; _+_; _∸_; compare; less; equal; greater)
open import Relation.Nullary using (Dec; yes; no)
open import Data.List using (List; _++_; _∷_; []; [_]; map)
open import Data.Maybe using (Maybe; just; nothing)
data Ty : Set where
-- irrelevant for bug
Con = List Ty
index : List Ty → ℕ → Maybe Ty
index _ _ = nothing -- irrelevant
data Tm : Set where
V : ℕ → Tm
subst-shift : Tm → ℕ → Tm → Tm
subst-shift (V x) n new with compare x n
... | less .x k = V x
... | equal .x = new
... | greater .n k = V (x ∸ 1)
data _⊢_⦂_ : Con → Tm → Ty → Set where
⊢V : ∀ {Γ x t} →
index Γ x Eq.≡ just t →
Γ ⊢ V x ⦂ t
subst-shift-pres : ∀ {Γ tm sub ty₁ ty₂} →
Γ ⊢ tm ⦂ ty₁ →
(ty₂ ∷ Γ) ⊢ subst-shift tm 1 sub ⦂ ty₁
subst-shift-pres {Γ} {V x} {sub} {ty₁} {ty₂} ⊢tm with compare x 1 in eq
... | k = {!!}
I hope this bug report is beneficial.
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