もっともっと使われると、変わるんでしょうかね

まぁぼくはどこにもフィードバックしてないので、ユーザとして認識されてないんですけど、こういうのは凄く頭のいい、普通の人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が)ウルトラやバイ。