1

私には目標があります

quad X Y

、しかし、「クワッド」の定義を覚えていないので、その定義の検索を開始したくありません。

quad をその定義にすばやく置き換えることができる戦術はありますか?

 Record quad (X Y:Type):= { x:X; y:Y}.

または、覚えて使用する必要があります

refine (@Build_quad _ _).

?

4

1 に答える 1

3

少し間違ってBuild_quadいるのは の定義ではなく、quadそのコンストラクタです。タイプの用語を作成しますquad。@ejgallego が言ったようにconstructor、この状況では戦術を使用する必要があります。

あなたの目標は type の用語を提供することを望んquad X Yでおり、そのような用語をゼロから構築する唯一の方法はBuild_quad、 typeのコンストラクターを使用することforall X Y: Type, X -> Y -> quad X Yです。

于 2016-06-01T08:45:19.247 に答える