标签: agda-mode

我正在尝试编译一个 Agda 文件，但是我无法让它找到标准库。我在这里看过文档。

我使用 Stack 来安装它：

> which agda
/home/joey/.local/bin/agda

我已经为我的 Agda 目录设置了环境变量：

> echo $AGDA_DIR
/home/joey/.agda

其中填充了正确的文件：

/home/joey/agda/agda-stdlib/standard-library.agda-lib

> cat "$AGDA_DIR"/libraries
/home/joey/agda/agda-stdlib/standard-library.agda-lib

> cat "$AGDA_DIR"/defaults
standard-library

> cat /home/joey/agda/agda-stdlib/standard-library.agda-lib
name: standard-library
include: src

但是，当我去编译 Agda 文件时，出现以下错误：

Failed to find source of module Function in any of the following
locations:
  /home/joey/agda/AutoInAgda/src/Function.agda
  /home/joey/agda/AutoInAgda/src/Function.lagda
  /home/joey/.stack/snapshots/x86_64-linux-nopie/lts-8.14/8.0.2/share/x86_64-linux-ghc-8.0.2/Agda-2.5.2/lib/prim/Function.agda
  /home/joey/.stack/snapshots/x86_64-linux-nopie/lts-8.14/8.0.2/share/x86_64-linux-ghc-8.0.2/Agda-2.5.2/lib/prim/Function.lagda
when scope checking the declaration
  open import Function

我如何告诉 Agda 去哪里寻找标准库？这是因为堆栈的问题吗？

我在 Ubuntu 17.10 上，如果这有区别的话。

我正在使用agda进行编程语言基础的练习考试,它有以下问题:

您将获得以下Agda声明:

data Even : N ? Set where
 ezero : Even 0
 esuc : { n : N }  ? Even n  ? Even (2+ n)

假设已导入标准自然数库.回答以下的问题:

a)什么类型的ezero？

b)是否有任何类型的条款Even 1？

c)有多少个类型Even 2？列出他们

d)描述一个潜在的问题,如果我们改变esuc的返回类型Even (n+2)而不是Even (2+n).

我们没有提供解决方案手册.这个问题似乎很基本,但我不确定这些问题.我认为前三个的答案是:

一套

b)没有类型的条款偶数1

c)一个类型的偶数2

d)不知道

对这些问题的回答以及简要说明将受到高度赞赏.谢谢