Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Question

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Question


Chronological Thread 
  • From: Richard Dapoigny <richard.dapoigny AT univ-savoie.fr>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Question
  • Date: Sun, 09 Mar 2014 11:26:21 +0100

Hi all,
I have some problem with operational type classes. Consider the following fragment:

Class N       := nn :> Type.
Class singular.
Parameter M1 : singular -> N. Coercion M1 : singular >-> N.
Class plural.
Parameter M2 : plural -> N. Coercion M2 : plural >-> N.
Class empty.
Parameter M3 : empty -> N. Coercion M3 : empty >-> N.

Parameter Association : relation N.

Parameter is_one_of : relation N. (* argument filtering on the relation *)
Class epsilon (A:singular)(b:N) := eps :> is_one_of A b.

Class LO_exist_at_least (a:singular){A:singular}{e:epsilon A a}.
Variable A    : singular.
Variable B    : singular.
Variable ert  : epsilon A B.
Variable ert' : epsilon B A.
Variable e1   : empty.
Variable p1   : plural.
Variable ert1 : epsilon A p1.
Variable d1   : LO_exist_at_least_plural B.

with the following error:
Error:
Unable to satisfy the following constraints:
?67 : "epsilon ?66 B"
?66 : "singular"

However, it works with A. Is anybody has an idea?
Thanks in advance,
Richard

--

JPEG image

begin:vcard
fn:Richard Dapoigny
n:Dapoigny;Richard
email;internet:richard.dapoigny AT univ-savoie.fr
tel;work:+33 450 09 65 29
tel;cell:+33 621 35 31 43
version:2.1
end:vcard




Archive powered by MHonArc 2.6.18.

Top of Page