[Agda] open import public

[Andrew Pitts]

On 29 May 2015 at 09:44, Leonhard Markert <lm510 at cam.ac.uk> wrote:
> Hello Andy,
>
> This probably doesn't really answer your question---but your code
> type-checks if you put "module ${filename minus .agda extension} where"
> at the beginning of each file...

Well, I think that answers my question rather well.

I have got used to Agda's recently acquired ability to pick up the
top-level module name within a file from the file name, but that seems
to be what is causing my "public" problem.

Thanks,

Andy