Open
Description
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!