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