Coqの製品タイプ

Question

coqの製品タイプにパラメータを渡す際に問題があります。私はのように見えるの定義、

Definition bar (a:Type) := a->Type. 

が、私は彼らの製品/順序対を出力「A」と「バーA」とによって作られたもので受け取る関数を定義する必要があります。だから私は次のことを試みた。

用語「b」は、それが型を持つことが予想される一方で、「タイプ」「バー」型を持つ私にエラー

を与える

Definition foo (a:Type)(b:bar a):= prod a b. 

。

は本当にここで混乱していますがこのこと、

Definition foo (a:Type) := prod a (bar a). 

作品だけで結構です。明らかに 'bar a'には 'Type'という型があるので、元の定義を修正する方法がわかりません。私は変数を適切に渡していないと思う。

Answer 1

あなたfoo定義でbar aを展開し、エラーを表示するには：

Definition foo (a:Type)(b:a->Type):= prod a b. 

今ではbがタイプではないことを明確にする必要があり、それはaからTypeの機能です。

aのオブジェクトを取得しないため、bを何にでも適用することはできず、Typeを取得することはできません。それが動作する理由

2番目の定義は、以下を参照してくださいするには、再度展開します

Definition foo (a:Type) := prod a (a->Type). 

両方aとa->Typeは、製品の有効なType年代です。