Agdaなんかすごそう

How to install

Ubuntuでは

sudo apt install agda-mode

Archlinuxでは

sudo pacman -S agda

ArchlinuxではEmacsの設定ファイル ~/.emacs.d/init.el に

;; Agda-mode
(load-file (let ((coding-system-for-read 'utf-8))
                (shell-command-to-string "agda-mode locate")))
(load-library "agda2")

を書いておこう。 Terminal上で書こうとするとUTF-8がえらいことになるので X転送推奨。

Agdaで足し算

自然数を定義します。

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

zero が0, suc が +1 する関数。

足し算を定義します。

_+_ : Nat -> Nat -> Nat
n + zero = n
n + suc m = suc (n + m)

適当に数を用意します。

two   = suc (suc zero)
three = suc (suc (suc zero))

足します。

x = two + three

EmacsでC-c C-nを押して x を表示させると、

suc (suc (suc (suc (suc zero))))

となってめでたく足し算ができました。

で？

もうちょっと強そうな話はまた書きます。

参考文献