Consider the following file:
open import Agda.Builtin.Nat suc' = suc data D : Nat → Set where c : (@0 n : Nat) → D (suc' n) foo : (n : Nat) → D n → Set foo n (c _) = ?
Agda complains:
I'm not sure if there should be a case for the constructor c,
because I get stuck when trying to solve the following unification
problems (inferred index ≟ expected index):
suc' n ≟ n₁
Possible reason why unification failed:
Cannot solve variable n of type Nat with solution suc' n₁ because
the solution cannot be used at relevant, unrestricted modality
when checking that the pattern c _ has type D n
However, replacing suc' by suc in the type of c makes the file pass the typechecker.
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