The following example files do not give rise to an error message, even though they should.
File Bug.agda
:
module Bug where open import B1 open import B2 b : Set b = a
File B1.agda
:
module B1 where postulate a : Set
File B2.agda
:
module B1 where postulate a : Set
There is no module named B2
, and if there was then the use of a
in Bug
would be ambiguous.
Page last modified on October 16, 2007, at 12:30 pm
Powered by
PmWiki