Agda-2.3.2.2: test/succeed/Issue420.agda
-- named arguments should be allowed in module applications
module Issue420 where
module M {A : Set₁} where
open M {A = Set}
-- named arguments should be allowed in module applications
module Issue420 where
module M {A : Set₁} where
open M {A = Set}