んもー
natRight : {a : Nat} {b : Nat} -> a NatPair b -> Nat natRight (a natPair b) = b getNatRight : {a : Nat} {b : Nat} -> a NatPair b -> Val b getNatRight (a natPair b) = val b valNat : (a : Nat) -> Val a valNat a = val a body : (length (filter p xs')) NatPair (length xs') body = filterproof {X} {p} { xs'} right : Val (length xs') right = getNatRight body
これだと良いのに
right' : Nat right' = natRight body -- body = filterproof right : Val (length xs') right = valNat right'
これだとダメだなんて・・・。
しんきんぐたーいむ
これはエラーとしては
natRight filterproof != length xs' of type Nat when checking that the expression valNat (natRight body) has type Val (length xs')
というのが出てて、
body = filterproofだというのはそうで、
right' = natRight body = natRight filterproof
とみると、valNatの定義から
right : Val (natRight filterproof)
で自明じゃないので、確かにそうなりますっていう。
しかしながら気持ちとしては
right' = natRight body
から
right' が length xs'であって欲しい
と思っていて、そうすると
right = val right'
でunify可能だよなーとか。
ただそれは、「値の話」なので「実行されて」はじめて分かる事で、そうするとやっぱり型だけで片付けられないと困るんですけど、上のだとガチガチなのでうーんとか。
少なくとも構成物のうちにリテラルが含まれている場合は、それはどうも実行してくれて型レベルのパラメタに活かしてる気がしますけど。勘て感じです。
まぁガンガンad-hocに書いていってみるかな。