coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
- [Coq-Club] Problem using a functor, Emmanuel Polonowski
- Re: [Coq-Club] Problem using a functor, Adam Chlipala
- Re: [Coq-Club] Problem using a functor, Emmanuel Polonowski
- Re: [Coq-Club] Problem using a functor, Adam Chlipala
Archive powered by MhonArc 2.6.16.