Agda

OSの採点を Twitter で愚痴りながらやってますが、

＊　圏論のFreyd's Ajoint Functor Theorem

が、まだだったのを思い出した。そういえば、

＊ Haskell と Agda がinstallされてない

普通に install して入るんだけど、

＊ epkg の方が良くね?

ってことなんですが、

Haskell/Agda は、User home の下に入れるようになってる

なのですが、

cabal --global

ってのがあるらしい。それで順調だったのですが、

cpphs がない

とかおっしゃる。良く分からなかったんだけど、

/Library/Haskell/bin

にあるのを make の path に教えてやらないとだめらしい。

で、Agda は入ったんですが、

agdaのstdlibがない

で、それもpackageにしたんだけど、

permisson がない

え? そうか、agdai とかを作るので、それを共通 directory に置くことはできないらしい。いや、agdai を作ってやればできるのかも。でも、

方法がわかりません

いや、もう少し追求すればわかるかもしれないが、まぁ、いいや。一応、動いたし。