coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] module derivation - again

From: "Elie Soubiran" <soubiran AT lix.polytechnique.fr>
To: "Julien Tesson" <julien.tesson AT univ-orleans.fr>
Cc: "Mailing list Coq" <coq-club AT pauillac.inria.fr>
Subject: Re: [Coq-Club] module derivation - again
Date: Tue, 7 Oct 2008 17:13:48 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:sender:to:subject:cc:in-reply-to:mime-version :content-type:content-transfer-encoding:content-disposition :references:x-google-sender-auth; b=dDOjEnrGmY1QhNUNSLeTRooAeOGbtmPUyw5gkoh0tsclYHkmDTEuYUqJ0lbjKl1cL8 yozQkqI48DBlMRn7Ydzt0wEx9r6O47yg8IyiXPcFlYPw5CbVviH6umP3wGwmEwPI7p4v mlnZrTPZUaKpyqvddvzi6H9hQ/3vgLg7VfR1I=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hello,

> Shouldn't it be of type (B1 A) and have a field b1 ?

No, in your fonctor test the type of the module ba is :

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

this the resulting type of the application of (b_impl : B) by (a_impl : A).

Elie

[Coq-Club] module derivation - again, Julien Tesson
- Re: [Coq-Club] module derivation - again, Elie Soubiran
  - Re: [Coq-Club] module derivation - again, Julien Tesson