[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