[Agda] Failed to find source of module
Sergei Meshveliani
mechvel at botik.ru
Mon Feb 13 14:49:30 CET 2017
Dear Agda developers,
when I set to the directory ~/mySource/Foo/ the file TT.agda, with
the heading
module TT where
(instead of the correct module Foo.TT where),
Agda 2.5.2 reports
(*) Failed to find source of module ...
And it lists the directory names where it searched, and the directory
~/mySource is not listed.
If I improve the name to Foo.TT, then it searches where it is needed.
And the error report (*) looks as misleading.
Regards,
------
Sergei
More information about the Agda
mailing list