Normalmente vejo a importdiretiva no Idris usada em um .idrarquivo. Mas no código aqui , vejo uma instância importusada em um diretório.
import public Text.Lexer
, onde Text.Lexer é um diretório contendo apenas um arquivo chamado Core.idr.
Não consegui encontrar documentação para tal uso. O tutorial não parece dizer que é possível importar um diretório ou o que isso significa.
Alguém pode ajudar a explicar o significado da diretiva import aqui no diretório?
Também existe um arquivo
Text/Lexer.idrneste repositório.import Text.Lexersimplesmente importa este único arquivo. Um diretório não pode ser importado.É comum no Idris e em linguagens relacionadas ter um módulo
Ae alguns módulos aninhados emA. A linguagem não impõe nenhuma relação; isso é feito exclusivamente para fins organizacionais.