10

Agda で型階層がどのように機能するかを理解しようとしています。

セット型 X を定義するとします。

X : Set

そして、誘導型の構築に進みます

data Y : X -> Set where

の型はX -> Set何ですか? それはセットですか、それともタイプですか？

ありがとうございました！

4

1 に答える 1

12
于 2013-04-10T13:50:22.493 に答える