[Agda] Beginner's Troubles With Documentation

[Robin Green]

At Thu, 17 Sep 2009 12:18:01 +0100,
Nils Anders Danielsson wrote:
> > 5. Why open and import separated into two language constructions instead 
> > of one as in many other languages?
> 
> The import keyword brings names into scope qualified, and open brings
> qualified names into scope unqualified.

And of course modules can be defined that are nested into the current module, so in that case you'd want to use open but not import. This can be particularly useful for records (which automatically create corresponding modules for themselves).
-- 
Robin