OpenModule.agda

module OpenModule where

module A where
  postulate X : Set

-- Both open import and open module applies the directives
-- to the "open" rather than to the module.
open import Nat   hiding (zero) renaming (Nat to N)
open module B = A renaming (X to Y)

Test : Set
Test = Y → B.X → N → Nat.Nat

zero : N
zero = Nat.zero

-- If the module isn't opened the directives are applied to
-- the module.
import Nat as N renaming (Nat to N)
module C = A    renaming (X to Z)

Test₂ : Set
Test₂ = N.N → C.Z