PublicWithoutOpen2.err

PublicWithoutOpen2.agda:3,8-17
The public keyword must only be used together with the open keyword
when scope checking the declaration
  import Imports.A public