typeclass - Coq 部分 : require typeclass instance

Question

Require Import Relations RelationClasses.

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

我如何要求 R 是偏序？

Answer 1

有 Context 语法，参见 Coq 引用手册，§20.4 :

To ease the parametrization of developments by type classes, we provide a new way to introduce variables into section contexts, compatible with the implicit argument mechanism. The new command works similarly to the Variables vernacular (see 1.3.1), except it accepts any binding context as argument.

例子:

From Coq Require Import RelationClasses.

Generalizable Variable A eqA R.

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