I am trying to use the Programming Language Foundation with Agda plfa library, however the import does not appear to be working properly.
I have cloned the repository and added the repository path to: ~/.agda/libraries and plfa to ~/.agda/defaults.
When I create a test.agda file and check a single line
module plfa.part1.Naturals where
I get an import error:
You tried to load /Users/johngfisher/Desktop/agda_test/nats.agda
which defines the module plfa.part1.Naturals. However, according to
the include path this module should be defined in
/Users/johngfisher/agda_env/libraries/plfa/src/plfa/part1/Naturals.lagda.md
The file is present in the location the import is coming from so I am unsure of why Agda is unable to find it. Any help would be appreciated.
module plfa.part1.Naturals where
defines a module named plfa.part1.Naturals
Did you mean to type
module test where
open import plfa.part1.Naturals
instead?