The following code triggers an internal error when trying to use Mimer (C-c C-a) in either of the last two holes:
open import Agda.Builtin.Nat
open import Agda.Builtin.Sigma
data ⊥ : Set where
_×_ : (A B : Set) → Set
A × B = Σ A (λ _ → B)
impossible : Nat → Nat → ⊥ × ⊥
impossible m zero = {!!}
impossible m (suc n) =
let _ , _ = impossible {!!} n
in {!!} , {!!}
This is the error:
An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at
src/full\Agda\TypeChecking\Monad\Context.hs:139:32 in
Agda-2.8.0-9u1uvJH0I89CZ4mhZl7o05:Agda.TypeChecking.Monad.Context
The error happens both on version 2.7.0.1 and on latest master.
None of the following versions trigger the error:
impossible₁ : Nat → Nat → ⊥
impossible₁ m zero = {!!}
impossible₁ m (suc n) =
let _ = impossible₁ {!!} n
in {!!}
impossible₂ : Nat → ⊥ × ⊥
impossible₂ zero = {!!}
impossible₂ (suc n) =
let _ , _ = impossible₂ n
in {!!} , {!!}
impossible₃ : Nat → Nat → ⊥ × ⊥
impossible₃ m zero = {!!}
impossible₃ m (suc n) =
let _ = impossible₃ {!!} n
in {!!} , {!!}
impossible₄ : Nat → Nat → ⊥ × ⊥
impossible₄ m zero = {!!}
impossible₄ m (suc n) =
let _ , _ = impossible₄ {!!} n
in {!!}
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