module Modules where import TestDir.Testing hole : {!!} hole = TestDir.Testing.myidentifier -- Here is a file. -- Within this file, we will define some submodules: postulate X : Set module A where postulate A : Set postulate x : A module B where postulate B : Set postulate x : B module C where postulate C : Set private postulate y : B postulate z : C module D where postulate D : Set postulate y : B postulate w : D postulate x : X open A open B.C using () renaming (z to z') module VeryComplicatedName where postulate Y : Set postulate Z : Set postulate W : Set postulate a b c : Y postulate d e f : Z module V = VeryComplicatedName module W where open VeryComplicatedName public -- Names from VeryComplicatedName are available locally here test : {!!} test = Z open W open import Equality -- The identifiers a, W.a, V.a VeryComplicatedName.a are all defined. theorem : VeryComplicatedName.a == V.a theorem = refl