a should be in scope after B' has been opened:
module Bug where
module A where
postulate a : Set
module B (b : Set) where
open A public
module C where
postulate c : Set
module B' = B c
open B'
d : Set
d = a
Error message:
Bug.agda:16,7-8
Not in scope:
a at Bug.agda:16,7-8
when scope checking a
Fixed.
Page last modified on October 16, 2007, at 09:38 am
Powered by
PmWiki