Agda Installation PLFA Configuration

Question

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.

Answer 1

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?