2

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.

Ethan
  • 876
  • 8
  • 18
  • 34
John Fisher
  • 243
  • 3
  • 10

1 Answers1

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

gallais
  • 11,823
  • 2
  • 30
  • 63