Require Import Relations RelationClasses.
Section MySection.
Variable A : Type.
Variable R : relation A.
(* ... *)
End MySection.
How could I require R
to be a partial order?
Require Import Relations RelationClasses.
Section MySection.
Variable A : Type.
Variable R : relation A.
(* ... *)
End MySection.
How could I require R
to be a partial order?
There is the Context
syntax, see The Coq Reference manual, §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.
Example:
From Coq Require Import RelationClasses.
Generalizable Variable A eqA R.
Section MySection.
Context `{PO : PartialOrder A eqA R}.
(* ... *)
End MySection.
Generalizable Variable
, see Implicit generalization in the Ref. Man.