Cubical Agda

{-# OPTIONS --cubical-compatible --safe #-}

の修正は終わったんだが、

UnsupportedIndexedMatch の警告を抑制してた

Cubical は Homotopy Type Therory と関係あるらしく、無視しようかと思ってたんですが

量多いし。でも、

　どうも、理論的には少し工夫すると消せるらしい

つまり、with による data の場合分け、つまり、単一化の複雑度の問題なわけね

これを避けると、実は少し見通しが良くなる

なので、取る方向かな。ついでに Cubical Agda を少し学ぶか