Agda-2.3.2.2: test/fail/ModuleDefinedInOtherFile.agda

module ModuleDefinedInOtherFile where

import Imports.B