The Coq mailing list

[Frédéric Besson <frederic.besson AT inria.fr>]

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