まぁぼくはどこにもフィードバックしてないので、ユーザとして認識されてないんですけど、こういうのは凄く頭のいい、普通の人100人分ぐらいの人達が使ってるので多分大丈夫のはず module TCheckTest where data Nat : Set0 where zero : Nat succ : Nat -> …

割と良く分からないなーって感じになって、ググるとさかいさんの記事が出て来たので、依存和使っててすごいというか、なんで依存和使ってるか分からん感じだったんですけれども、実際やってみると少し分かりました。http://www.tom.sfc.keio.ac.jp/~sakai/d/…

module Proof1 where data List (A : Set0) : Set0 where [] : List A _::_ : A -> List A -> List A rec1 : {X : Set0} -> List X -> List X rec1 [] = [] rec1 (x :: xs) = rec1 [] -- ここのrec1でrec1の停止性を証明出来ないらしい。うーん・・・。 rec1…