今回は Constant Definitions から Parametric Sets まで。 Constant Definitions nine : ℕ nine = suc (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))) ten : ℕ ten = suc nine (定数名) = (式) の形式で定数を定義することができます。 定義の前行…

Agda Tutorial を読んで、自分なりにまとめたメモ。 今回は Modules から Recursive Sets まで。 Modules すべての Agda module は以下の形式のヘッダから定義が始まります。 module Modules.Basic where module と where は Agda の keyword (予約語) モジ…

Ubuntu 16.04 に Agda をインストールする Ubuntu 16.04 上に Agda と推奨開発環境の Emacs をインストールします。 なお Emacs の設定を簡単に済ませるために Spacemacs を使用します。 Spacemacs を使用しない場合は Agda 2 Readme にしたがって Emacs の…