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