Agda の std-lib 2.0

一応、群論の方はなおせんたんだが、いろいろ判明。

　　--cubical-compatible では、case 文と Termination check に問題がある

なので、case文の方は

　--warning=noUnsupportedIndexedMatch

で警告を消す。Termination check は　cubical-compatible 諦めるしかないっぽい。

まぁ、cubical-compatible のありがたみは特にないわけなんですが。

--safe の方は、ほとんど問題無し。なんなんでしょうね。


問題は、

　　Data.Fin の 関数の zero / suc への展開が全滅

with f x とかやるだけで、

　 Function.Bundles.Inverse.from perm (suc x) != w of type Fin (suc n)

意味不明らしい。

いや、もともと Data.Fin (有限な自然数)怪しくてな。workaroundはできたんですが、大変だった...

finiteSet とかでもとらぶる予感。でも、無理になおさなくてもいいとも思うんですが。まぁ、ちまちまなおすか。