'Agda Installation PLFA Configuration

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.

agdaagda-modeagda-stdlib


Solution 1:[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?

Sources

This article follows the attribution requirements of Stack Overflow and is licensed under CC BY-SA 3.0.

Source: Stack Overflow

Solution Source
Solution 1 gallais

Related Questions