コアセクション：タイプインスタンスインスタンスが必要

Question

Require Import Relations RelationClasses. 

Section MySection. 
    Variable A : Type. 
    Variable R : relation A. 
    (* ... *) 
End MySection. 

Rを部分的な順序にするにはどうすればよいですか？

Answer 1

ありContext構文は、Coqのリファレンスマニュアルを参照して、§20.4：

型クラスによって、開発のパラメータ化を容易にするために、我々は、暗黙的に対応して、セクションのコンテキストに変数を導入するための新しい方法を提供します引数のメカニズム。新しいコマンドは、バインドコンテキストを引数として受け付けることを除いて、Variables（1.3.1を参照）と同様に機能します。

例：

From Coq Require Import RelationClasses. 

Generalizable Variable A eqA R. 

Section MySection. 
    Context `{PO : PartialOrder A eqA R}. 
    (* ... *) 
End MySection.