Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] A module cannot be applied to another module application

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] A module cannot be applied to another module application


Chronological Thread 
  • From: Frédéric Besson <frederic.besson AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] A module cannot be applied to another module application
  • Date: Mon, 03 Jul 2017 13:41:56 +0200
  • Organization: Inria


On Mon, 2017-07-03 at 11:28 +0200, Chantal Keller wrote:
> Hi Frédéric,
>
> Thanks for your answer. This works if the nested application is in
> the
> resulting signature of the module, but how to deal with arguments?
> See e.g.
>
> Module Id' (T:TYPE) (B1:ID T) (B2:ID (Copy T)).

It seems you can do the same.

Module Id' (T:Type) (B1 : ID T).
Module CT := Copy T.

Module Id'' (B2 : ID CT).

--
Frédéric




>
> Best
> Chantal
>
>
>
> Le 03/07/2017 à 10:01, Frédéric Besson a écrit :
> > Hi Chantal,
> >
> > What about having an inner module?
> >
> > Module Id (T:TYPE) (B:ID T).
> >   Module CT := Copy T.
> >   Module IId <: ID CT.
> >     Parameter id : CT.t -> CT.t.
> >   End IId.
> > End Id.
> >
> >
> > Best,
> > --
> > Frédéric
> >
> >
> > On Sun, 2017-07-02 at 23:37 +0200, Chantal Keller wrote:
> > > Hi,
> > >
> > > This example is useless, but I would like to do domething similar
> > > to:
> > >
> > >
> > > Module Type TYPE.
> > >   Parameter t : Type.
> > > End TYPE.
> > >
> > > Module Copy (T:TYPE) <: TYPE.
> > >   Definition t := T.t.
> > > End Copy.
> > >
> > > Module Type ID (O:TYPE).
> > >   Parameter id : O.t -> O.t.
> > > End ID.
> > >
> > > Module Id (T:TYPE) (B:ID T) <: ID (Copy T).
> > >
> > >
> > > Coq 8.6 complains about the last statement: "Error: A module
> > > cannot
> > > be
> > > applied to another module application or with-expression; you
> > > must
> > > give
> > > a name to the intermediate result module first."
> > >
> > > How can I give a name to the nested application since I want to
> > > use
> > > it
> > > in the signature?
> > >
> > > Thanks
> > > Chantal



Archive powered by MHonArc 2.6.18.

Top of Page