functional-programming - 无法在 agda 中安装默认库

Question

尝试遵循本指南：https ://plfa.github.io/GettingStarted/

在“检查 Agda 标准库是否安装正确”之后的部分得到这个：

$ agda -v 2 nats.agda
Checking nats (C:\Users\AuSeR\agda\nats.agda).
C:\Users\AuSeR\agda\nats.agda:1,1-21
Failed to find source of module Data.Nat in any of the following
locations:
  C:\Users\AuSeR\agda\Data\Nat.agda
  C:\Users\AuSeR\agda\Data\Nat.lagda
  C:\Users\AuSeR\agda\.stack-work\install\5f9701df\share\x86_64-windows-ghc-8.8.3\Agda-2.6.1.1\lib\prim\Data\Nat.agda
  C:\Users\AuSeR\agda\.stack-work\install\5f9701df\share\x86_64-windows-ghc-8.8.3\Agda-2.6.1.1\lib\prim\Data\Nat.lagda
when scope checking the declaration
  open import Data.Nat

试图查看库文件的位置：

$ agda -l fjdsk Dummy.agda
 Library 'fjdsk' not found.
 Add the path to its .agda-lib file to
   'C:\Users\AuSeR\AppData\Roaming\agda\libraries'
 to install.
 Installed libraries:
   (none)

库文件如下所示：

C:\Users\AuSeR\agda\agda-stdlib\standard-library.agda-lib

像这样的默认值：

标准库

标签： functional-programmingagda