[Agda] open import public

[Leonhard Markert]

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...

  Leo

Andrew Pitts <Andrew.Pitts at cl.cam.ac.uk> writes:

> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda