Agda と格闘中

同じ所廻っているような気がする〜

やっぱりドキュメント読まないと。

https://agda.readthedocs.io/en/v2.5.4.1/language/with-abstraction.html

と思ったら、今使っているのは2.5.2なので既に古いらしく。2.5.3 からとか書いてあって。

まぁでも、

　　brew update
　　brew upgrade agda

ですむから簡単ですよね。と思ったら、

　　illegal byte code

はぁ? ちょっと困りましたが、

　　~/.agda/libraries

に library の場所が、そのまま書いてあるのか。これを

　　/usr/local/Cellar/agda/2.5.4.1/lib/agda/standard-library.agda-lib

に修正しろと。そう、brew upgrade agda が表示してました。

ω automaton で n 番目みたいなのを証明しにいくわけなんだけど、こっちは n, n-1, n-2 ... 1, 0 と推論するんだが、
ω automaton の計算の方は 0, 1, 2 と進んでいく。その辺が、うまく揃わなくって。

まぁ、そのうち、なんとかなるでしょう...