Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Problem using a functor

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Problem using a functor


chronological Thread 
  • From: Adam Chlipala <adamc AT csail.mit.edu>
  • To: Emmanuel Polonowski <polonowski AT u-pec.fr>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Problem using a functor
  • Date: Tue, 30 Aug 2011 08:12:21 -0400

Emmanuel Polonowski wrote:
When using the module system in order to instantiate a functor, I get a 
strange error message.

[...]

Module GI (a : A) := G a (FI a).

Error: Application to not path.

A path is a base module with a series of projections out of it. A path can't contain a functor application, and the argument in a functor application must be a path. So, actually quite a good error message once the definition is made clear!

Here's an alternate declaration which I would assume is equivalent to what you wanted to write:

Module GI (a : A).
  Module FI' := FI a.
  Module G' := G a FI'.
  Import G'.
End GI.




Archive powered by MhonArc 2.6.16.

Top of Page