はじめに
知り合いの元プログラマが一年に１つずつ新しい言語を触ってみると良い、とのたまってくれたので、新しい言語にチャレンジしようと思います、てなわけでAgdaをチョイス。
ちなみに去年（まで）はマイナーな項書き換え言語とMaxima で記号処理と数値代入を、Haskell を趣味で勉強してました。
理由は特に無いが、趣味で圏論とHaskellをやっているのでその延長で。
文法似ているのでとっつきやすいかなというだけ、あとはちょっと触ってみたいコンテンツがあったので、こことかこことか。
定理証明（支援）
別にソフトウェア開発をしているわけでもないのだが、Haskell のいうところのIt’s a truism within the Haskell community that once code compiles, it’s more likely to work correctly than in other languages.を"ちゃんと"するといわゆる定理証明システムになる（らしい）。
もちろんCoq も候補にあったがなんとなく敬遠してしまった、なんとなく。
誰も書かないCoq入門以前の話を見ちゃって気後れしてしまったのもある、なんかややこしそう。。。
あと最近出たらしいLeanもかっこよかったのだけど、まぁ又の機会に。
しかし公式ページとロゴがかっこいい、量化子か。
やや教材が少ない気がするのが気がかりだが。
導入
オフィシャルに則ってさくっとAgda 本体とAquamacsを導入、問題は普段vim を（カッコつけて）使っているので使えるかなぁという点だけ、まぁずっと入力モードのvim と思ったら良いのかな？
実は保存とか終了とかも知らないので不安だったけど、なんとかなるでしょう。
Emacs
大文字のC がコントロールキーだということや終了の方法(C-x C-c)くらいしか知らなかったのでM ってなんやねん？となって愉快だった。
困ったらここを見たりしてる。
Standard Library
Standard Library を導入するのがやや困った、最終的には出来たけど。
まずはStandard Libraryの通りにやってみる、ここで
Insert the path DIR/src.
とあるので最初カレントディレクトリ(.)を消したうえでDIR/src だけ指してたが、こうすると自分が書いたファイルをDIR/srcに探しに行ってしまうので(.) とDIR/src にしなきゃいけませんでしたね、よく考えりゃアホなことをしてしまっていた。
Unicode
どうもなれないのがUnicode の多用、いい意味でなのだけどタイプが多くなるのがなぁ。。。
動かしてみる
どうもペアノの公理をためしてみるのが試金石みたい、ちと古いかもだけどHello, Peanoのように
module Recursive where
open import Enumerated using (Bool; true; false)
{-
Peano rep.
0 ~ zero
1 ~ suc (zero)
n+1 ~ suc n
-}
data ℕ : Set where
zero : ℕ
suc : ℕ → ℕ
おきまりのC-c C-d でsuc (suc zero) などの型を見てみてちゃんとℕ になってることを見る、が今のところだからどうした？という域を出ないな、、、