coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Julien Tesson <julien.tesson AT univ-orleans.fr>
- To: Mailing list Coq <coq-club AT pauillac.inria.fr>
- Subject: Re: [Coq-Club] module derivation - again
- Date: Tue, 07 Oct 2008 17:52:18 +0200
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
hi,
No, in your fonctor test the type of the module ba is :yes but in the fonctor test1 we know that ba is (b1_impl a_impl), which has type (B1 A) so why can't we deduce this type (which include B A) ?
sig Axiom b : a_impl.a->a_impl.a end
Is there a way to specify it ?
begin:vcard fn:Julien Tesson n:Tesson;Julien org;quoted-printable:Laboratoire d'Informatique Fondamentale d'Orl=C3=A9ans email;internet:julien.tesson AT univ-orleans.fr title:Doctorant tel;work:+33/(0) 2 38 41 72 68 tel;fax:+33/(0) 9 55 33 36 68 x-mozilla-html:TRUE url:http://tesson.julien.free.fr/ version:2.1 end:vcard
- [Coq-Club] module derivation - again, Julien Tesson
- Re: [Coq-Club] module derivation - again,
Elie Soubiran
- Re: [Coq-Club] module derivation - again, Julien Tesson
- Re: [Coq-Club] module derivation - again,
Elie Soubiran
Archive powered by MhonArc 2.6.16.