函数式编程进阶 1 - Agda 入门

内容提要

这是函数式编程进阶系列的第一篇文章,介绍了 Agda 的基本使用。

Agda 简介

Agda 是一种带有依赖类型的编程语言。由于带有强定型和依赖类型,Agda 可以作为证明助理,(在构造性设置下)证明数学定理并将这些证明当做算法来运行。

Agda 安装

Emacs 配置

推荐使用 Emacs 编辑 Agda 文件。首先安装 Emacs,然后安装 Agda 模式。

Emacs 使用

Agda 基础