coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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 --
|
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
- Re: [Coq-Club] Unintended behavior with (operational) typeclass, Julien Tesson, 03/01/2014
- Re: [Coq-Club] Unintended behavior with (operational) typeclass, Matthieu Sozeau, 03/07/2014
- [Coq-Club] Question, Richard Dapoigny, 03/10/2014
- Re: [Coq-Club] Unintended behavior with (operational) typeclass, Matthieu Sozeau, 03/07/2014
Archive powered by MHonArc 2.6.18.