Agda を {-# OPTIONS --cubical-compatible --safe #-} に書き換える作業なわけですが、
Red Black Tree 片付いたので、ZFの方をなおしているところ
引っかかるのは、functional-extentionality とか、非構成的な仮定を module の引数にするとかそんなの
あと、微妙に unification 関係に差がでるらしい。どれくらいの意味があるのかは実はよくわからない
割と順調だが、残りの4つが割と大物でな。Zorn と Topology と Tychonoff か
まぁ、復習になってよい説はある
これが終わったら、たぶん、Category 側もやります
＊ ＊ ＊
病院から戻ってきたら、夜、なんか熱出したので、少しお休み
風邪かと思ったら、今日には熱は引いてたんだが、まぁ、休んだ方がいいだろう
いつもの「休日ダウン」パターンだな
No comments:
Post a Comment