module Dummy where
import Dummy as D module M (A : Set) where
module Top where import M postulate A : Set open module MA = M A
In this example the typechecker doesn't think that M takes any arguments. If Dummy is imported without
as D then everything work fine.
- The problem is an implicit assumption that the name of the top-level module is the first name to be generated in a file.
Powered by PmWiki