もっともっと使われると、変わるんでしょうかね
まぁぼくはどこにもフィードバックしてないので、ユーザとして認識されてないんですけど、こういうのは凄く頭のいい、普通の人100人分ぐらいの人達が使ってるので多分大丈夫のはず
module TCheckTest where data Nat : Set0 where zero : Nat succ : Nat -> Nat data List (A : Set0) : Set0 where [] : List A _::_ : A -> List A -> List A data Val {A : Set0} : A -> Set0 where val : (a : A) -> Val a rec1 : List Nat -> List Nat -- rec1は当然停止性が証明されてない rec1 [] = rec1 (zero :: []) rec1 (x :: xs) = x :: (rec1 (x :: xs)) test : Val (rec1 ((succ zero) :: [])) test = val (rec1 ((succ zero) :: []))
停止性判定されてないとコンパイル出来ないとかいうんだったら、こういう型のパラメタに停止性判定されてないの持ってくるとかも出来ないようにして欲しいかもなーみたいなのは。
当然ですが、これでC-c C-lやるとemacsが(とうよりはバックグラウンドで走ってるghciが)ウルトラやバイ。