20070613-2

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