I'm working with an accessibility predicate defined as an inductive record, along with a recursive function over accessibility. It seems that different applications of that recursive function are then always equal when they shouldn't be (example minimized by @ncfavier):
open import Agda.Builtin.Equality
module _
(Level : Set)
(_<_ : Level → Level → Set) where
record Acc (k : Level) : Set where
pattern
inductive
no-eta-equality
constructor acc<
field acc : ∀ {j} → j < k → Acc j
open Acc
module _
(U' : ∀ k → (U< : ∀ {j} → j < k → Set) → Set) where
U< : ∀ {k} → Acc k → ∀ {j} → j < k → Set
U< (acc< f) {j} j<k = U' j (U< (f j<k))
lemma : ∀ {i j} (accj₁ accj₂ : Acc j) (i<j₁ i<j₂ : i < j) → U< accj₁ i<j₁ ≡ U< accj₂ i<j₂
lemma accj₁ accj₂ i<j₁ i<j₂ = refl
If an inductive datatype version of Acc is used, then there is the expected type checking error.
...
data Acc (k : Level) : Set where
acc< : (∀ {j} → j < k → Acc j) → Acc k
...
accj₁ != accj₂ of type Acc j
when checking that the expression refl has type
U< accj₁ i<j₁ ≡ U< accj₂ i<j₂
Agda version: 2.7.0.1-ae4464a
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