#またまたですが, agdaについて教えてください
#headとかtailに相当するものを定義したいとします
#total functionじゃないとダメだから
#この場合 head : {A : Set} -> List A -> Aはムリなので
#head : {A : Set} -> (xs : List A) -> {p : null xs == false} -> Aな感じでやろうとしましたが
#こういうのってよくないのでしょうか？ Data.Listにはそもそもhead,tailがありませんけど。
#で、Vec的にやろうと思いまして、List#を定義しました。
#data List# (A : Set) : N -> Set where...です。
#で、snoc : {A : Set} {n : N} -> A -> List# A n -> List A (suc n)を書いたところ
#snoc x xs = xs ++ [ x ]が
#n + suc zero != suc .nが自明ではないってことで型エラーになります。
#理由はまぁ分かるんですが、これどう処置すればいいんでしょう？
#List# A (n + 1)とかにすればOKというやつではなく、知りたいのは
#ここで n + (suc zero)がsuc nと同じことを教えてやるにはどうすればいいのかです。
haskell-ja > Archives > 2013/10/27