What does it mean to import a directory in Idris2?

Question

I usually see the import directive in Idris used on a .idr file. But in the code here, I see an instance of import used on a directory.

import public Text.Lexer

, where Text.Lexer is a directory containing only one file called Core.idr.

I couldn't find documentation for such usage. The tutorial does not seem to say that one can import a directory, or what it means.

Can someone help explain the meaning of the import directive here on the directory?

Answer 1

There is also a file Text/Lexer.idr in this repository. import Text.Lexer simply imports this single file. A directory cannot be imported.

It's common in Idris and related languages to have both a module A and some modules nested under A. The language imposes no relation; it's done purely for organizational purposes.