Agda安装PLFA配置

Question

我正在尝试使用https://plfa.github.io/ plfa库，但是导入似乎没有正常工作。

我已经克隆了存储库，并将存储库路径添加到：~/.agda/libraries和plfa到~/.agda/defaults。

当我创建一个test.agda文件并检查一行时

module plfa.part1.Naturals where

我收到一个导入错误：

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

文件存在于导入来自的位置，所以我不确定Agda为什么找不到它。任何帮助都将不胜感激。

Answer 1

module plfa.part1.Naturals where

定义一个名为plfa.part1.Naturals的模块

你是想打字吗

module test where

open import plfa.part1.Naturals

而不是？