On agda 2.6.4.1 and 2.6.4.3
module Bug {a}
where
open import Agda.Primitive using (lsuc; _⊔_)
open import Agda.Builtin.Sigma using (Σ; _,_)
open import Agda.Builtin.Nat using (Nat; suc)
data _≤′_ (m : Nat) : Nat → Set where
≤′-refl : m ≤′ m
≤′-step : ∀ {n} (m≤′n : m ≤′ n) → m ≤′ (suc n)
_<′_ : (m n : Nat) → Set
m <′ n = (suc m) ≤′ n
data Product {n : Nat} : Set a where
ne : Product
record LogRelKit : Set (lsuc a) where
constructor Kit
field
⊩U : Set a
⊩B : Set a
⊩ : Set a
⊩/_ : ⊩ → Set a
module LogRel (l : Nat) (rec : ∀ {l′} → l′ <′ l → LogRelKit) where
record ⊩₁U : Set a where
constructor Uᵣ
field
l′ : Nat
l< : l′ <′ l
record ⊩₁U/ : Set a where
constructor Uₜ₌
record ⊩ₗB : Set a where
constructor Bᵣ
eta-equality
⊩ₗΣ/_ :
([A] : ⊩ₗB) → Set a
⊩ₗΣ/_
Bᵣ = Σ Product λ pProd → Nat
data ⊩ₗ : Set a where
Uᵣ : ⊩₁U → ⊩ₗ
Bᵣ : ⊩ₗB → ⊩ₗ
⊩ₗ/_ : ⊩ₗ → Set a
⊩ₗ/ Uᵣ (Uᵣ l′ l<) = ⊩₁U/
⊩ₗ/ Bᵣ ΣA = ⊩ₗΣ/ ΣA
kit : LogRelKit
kit = Kit ⊩₁U ⊩ₗB
⊩ₗ ⊩ₗ/_
open LogRel public
using
(Uᵣ; Bᵣ; Uₜ₌;
module ⊩₁U; module ⊩₁U/;
module ⊩ₗB)
pattern Σₜ₌ pProd prop = pProd , prop
pattern Uᵣ′ a b = Uᵣ (Uᵣ a b)
mutual
kit : Nat → LogRelKit
kit ℓ = LogRel.kit ℓ kit-helper
kit-helper : {n m : Nat} → m <′ n → LogRelKit
kit-helper {m = m} ≤′-refl = kit m
kit-helper (≤′-step p) = kit-helper p
⊩⟨_⟩ : (l : Nat) → Set a
⊩⟨ l ⟩ = ⊩ where open LogRelKit (kit l)
⊩⟨_⟩∷/_ : (l : Nat) → ⊩⟨ l ⟩ → Set a
⊩⟨ l ⟩∷/ [A] = ⊩/ [A] where open LogRelKit (kit l)
transEqTerm : {l : Nat}
([A] : ⊩⟨ l ⟩)
→ ⊩⟨ l ⟩∷/ [A]
→ ⊩⟨ l ⟩∷/ [A]
transEqTerm (Uᵣ′ l′ (≤′-step s)) _ =
lemma (transEqTerm
? ?)
where
lemma : {l′ n : Nat} {s : l′ <′ n} →
⊩⟨ n ⟩∷/ Uᵣ′ _ s → ⊩⟨ suc n ⟩∷/ Uᵣ′ _ (≤′-step s)
lemma = {!!}
transEqTerm
(Bᵣ Bᵣ)
(Σₜ₌ ne p~r) = {!!}
transEqTerm = ?
Throws the error:
An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full/Agda/TypeChecking/Substitute.hs:140:33 in Agda-2.6.4.1-7xG50m7UQLK4krJEY6TPg:Agda.TypeChecking.Substitute
The error no longer happens if one adds {l = suc l} in the U case. Like this:
transEqTerm {l = suc l} (Uᵣ′ l′ (≤′-step s)) _ =
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