1
Section Definitions.
Definition eq_dec X := forall x y : X, {x=y} + {x <> y}.
Existing Class eq_dec.
(* Any function that uses eq_dec. Doesn't matter -- ↓ ↓ ↓ *)
Definition f {X: Type} {DecX: eq_dec X} (x y: X) := x = y.
End Definitions.
Section MySection.
Context {T: Type}.
Hypothesis TEqDec: eq_dec T.
Inductive myType :=
| C: T -> myType.
Instance myTypeEqDec : eq_dec myType.
Proof. ... Defined.
(* Everything is ok *)
Example example1: forall (t1 t2: myType), f t1 t2.
Proof. ... Qed.
End MySection.
Section AnotherSection.
Context {T: Type}.
Hypothesis TEqDec: eq_dec T.
(* Now I must explicitly specify this -- ↓ ↓ ↓ ↓ ↓ ↓ ↓ ↓ ↓ ↓ ↓ ↓
Example example2: forall (t1 t2: @myType T), @f _ (@myTypeEqDec _ TEqDec) t1 t2.
Proof. ... Qed.
End AnotherSection.
Comme vous pouvez le voir dans l'exemple 1, Coq est capable de trouver des informations d'instance sur myType. Mais après avoir changé la section, toutes les informations sur les instances disparaissent et je dois le spécifier explicitement. Donc, quand j'ai beaucoup de types-classes et d'instances, le code devient rapidement désordonné. Évidemment, je devrais remettre cette information dans le contexte. Quelle est la bonne façon de le faire?Coq: importer des informations sur les instances