packages feed

Agda-2.3.2.2: test/fail/ModuleDefinedInOtherFile.err

ModuleDefinedInOtherFile.agda:4,8-17
You tried to load
Imports/B.agda which defines
the module Imports.A. However, according to the include path this
module should be defined in
Imports/A.agda.
when scope checking the declaration
  import Imports.B