#引き続き，agdaです．
#data Vec (A : Set) : (n : Nat) -> Set whereの例なんですが
#consの定義で A -> Vec A n -> Vec A (suc n)って書いてもnがNot in scopeと言われますけど
#そもそもVec (A : Set) : (n : Nat) -> Setって言ってんだからNatを示すインデックスだって分からないのでしょうか？
#あるいはVec A (suc n)って返値を書いてるんだからNat型の変数だって分かってもよさそうに思うのですが．
#{n : Nat}って入れなきゃならないのは何故？
#"Not in scope"だからnの型がわからないのではなくnそのものがわからない
#あ、そうなんですが、それも含めてnの使われ方からnが何かを分かってくれてもよさそうな気がしませんかね。
#そこのところはサボってるだけなのか、それとも型システムとして推測不可能なのか。
haskell-ja > Archives > 2013/05/15