Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] module derivation - again

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] module derivation - again


chronological Thread 
  • 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 :

sig Axiom b : a_impl.a->a_impl.a end

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) ?
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




Archive powered by MhonArc 2.6.16.

Top of Page