packages feed

Agda-2.3.2.2: test/fail/Issue154.agda

-- The same name can not be exported more than once from a module.
module Issue154 where

module A where
  postulate X : Set

module B where
  postulate X : Set
  open A public