[Agda] open import public

[Andrew Pitts]

The Agda Reference Manual, when explaining Agda's ability to re-export
names from another module

<http://wiki.portal.chalmers.se/agda/agda.php?n=ReferenceManual.Modules#export>

gives an example where the modules are all within one file. (It's not
a very helpful example, in that the code does not type check).

I was hoping that the "public" modifier would work with file-based modules

<http://wiki.portal.chalmers.se/agda/agda.php?n=ReferenceManual.Modules#import>

But if I have three files, as attached, then foobar.agda fails to
check because "Not in scope: foo".

Probably I am doing something stupid. But what?

Andy
-------------- next part --------------
A non-text attachment was scrubbed...
Name: bar.agda
Type: application/octet-stream
Size: 23 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20150529/f3c04db9/bar.obj
-------------- next part --------------
A non-text attachment was scrubbed...
Name: foo.agda
Type: application/octet-stream
Size: 22 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20150529/f3c04db9/foo.obj
-------------- next part --------------
A non-text attachment was scrubbed...
Name: foobar.agda
Type: application/octet-stream
Size: 43 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20150529/f3c04db9/foobar.obj