PublicWithoutOpen.err

PublicWithoutOpen.agda:5,1-13
The public keyword must only be used together with the open keyword
when scope checking the declaration
  module B = A public