我正在嘗試將Programming Language Foundation 與 Agda 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 找不到它。任何幫助，將不勝感激。
uj5u.com熱心網友回復：
module plfa.part1.Naturals where
定義了一個名為plfa.part1.Naturals
你是想打字嗎
module test where
open import plfa.part1.Naturals
反而？
轉載請註明出處，本文鏈接：https://www.uj5u.com/net/536808.html
上一篇：重定向在命令列中走多遠？
下一篇：終止檢查失敗