[Agda] missing import overlap

Andreas Abel andreas.abel at ifi.lmu.de
Wed Jul 12 10:17:34 CEST 2017


No, that's fine.  You could say that the second import statement is 
redundant, but there is no overlap.

Haskell is also fine with it:

 > import Control.Monad.Writer
 > import Control.Monad.Writer


On 10.07.2017 20:30, Sergei Meshveliani wrote:
> People,
> I wonder: given
> 
>    open import Relation.Nullary
>    open import Relation.Nullary using (yes; no)
> 
> Agda does not report an overlap. Needs it?
-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/


More information about the Agda mailing list