When case-splitting on x in B.agda, we get the pattern (;A.A⁺.a x) which is a
parse error rather the completely valid (a x).
A.agda:
open import Level
module A {l : Level} (A : Set l) where
data A⁺ : Set l where a : A → A⁺
B.agda:
module B where
open import Agda.Builtin.Nat
open import A Nat
swap : A⁺ → A⁺
swap x = {!!}
Note that if we inline A.agda as a parametrised module defined in B.agda then
everything is fine!
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