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