coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Chantal Keller <chantal.keller AT wanadoo.fr>
To: coq-club AT inria.fr
Subject: [Coq-Club] A module cannot be applied to another module application
Date: Sun, 2 Jul 2017 23:37:26 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=chantal.keller AT wanadoo.fr; spf=None smtp.mailfrom=chantal.keller AT wanadoo.fr; spf=None smtp.helo=postmaster AT ext.lri.fr
Ironport-phdr: 9a23:QyjM9hfYUdZXC8FjwEsKcAlrlGMj4u6mDksu8pMizoh2WeGdxcqzYB7h7PlgxGXEQZ/co6odzbGH7Oa4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9GiTe5Y75+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6bpgRh31hycdLzM37mHZhNFzgqxVrh2uqABwzYHPbYGJNvdzZL/Rcc8USGdDWMtaSixPApm7b4sKF+cMI+ZYoJP7p1sStxS+ARSnCubxxT9Mgn/5w7c62PkmHA7a3AwvBdQOsGjOo9XxLqsSUv66zK3MzTrddfNbwjn855LOch87vP6MWrVwfdDfyUk1Dg7IiEibp4/9Pz6Ny+gBrWyW4/B9We+ti2MrsRx9rzi1ysojjITCm5gbxUre9SpjxYY4Pd24R1B/Yd6jCJZfqS6bN5dsTsMmWWFouTw2yrMcuZKjfSgKzoooxwLHZvCabYSF5gjvWPuTLDp4nn5pZbKyiwy9/ES4z+3zTMi00FJEripfldnMs2gA2ADT6sedTPt94l2u2TKV2wDQ9O5EJUQ0mrTBK5M6zL8/jJwTvl7eES/xn0X6lqGWdl889uiy9+vneqnmpoObN4Jslg7+Nb0ultWjDuQ8LwgBRHOW+f+81b3m5U32Wq9GjvwwkqnDsZDVP94XpqCjA1wd7oF24BGmSjyizd4wnH8dLVsDdgjUoZLuPgTlIPn+Ef67y3ehlDNm3biSNb3oBInEKj7AnbPlcKxV9EdawQY0ypZR/cQHWfk6PPvvVxqp55TjBRgjPlnszg==

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

[Coq-Club] A module cannot be applied to another module application, Chantal Keller, 07/02/2017
- Re: [Coq-Club] A module cannot be applied to another module application, Frédéric Besson, 07/03/2017
  - Re: [Coq-Club] A module cannot be applied to another module application, Chantal Keller, 07/03/2017
    - Re: [Coq-Club] A module cannot be applied to another module application, Frédéric Besson, 07/03/2017
      - Re: [Coq-Club] A module cannot be applied to another module application, Chantal Keller, 07/03/2017