agda の version up はだいたい終わり

一部、激ムズくらいましたが。

　　ライブラリの引数を変更されるとムカつくよね?!

Data.Fin の suc だけじゃなくて、inspect が新しい構文になったんだが、どうも一部の機能が低いまたはバグがあるらしく。

その部分を、case文の中で再証明すれば workaround できるのに気がつくのに少し時間がかかりました。

後は細かい問題だった。postulate / functional-extensinality があると、--safe は付けられない。

まぁ、少し分離したけど、虚しい気もする。module の入力にすれば形式的には逃げられる。