coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Vadim Zaliva <vzaliva AT cmu.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] A module cannot be applied to another module application or with-expression
Date: Thu, 21 Nov 2019 19:47:38 -0800
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=vzaliva AT cmu.edu; spf=Pass smtp.mailfrom=vadim.zaliva AT west.cmu.edu; spf=None smtp.helo=postmaster AT mail-io1-f53.google.com
Ironport-phdr: 9a23:PNypmRSe3jbmURn4+Sq7+DQtlNpsv+yvbD5Q0YIujvd0So/mwa69YBaN2/xhgRfzUJnB7Loc0qyK6vumADFbqsvQ+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aFRrwLxd6KfroEYDOkcu3y/qy+5rOaAlUmTaxe7x/IAi4oAnLq8UbgYVvJqkxxxbNv3BFZ/lYyWR0KFyJgh3y/N2w/Jlt8yRRv/Iu6ctNWrjkcqo7ULJVEi0oP3g668P3uxbDSxCP5mYHXWUNjhVIGQnF4wrkUZr3ryD3q/By2CiePc3xULA0RTGv5LplRRP0lCsKMSMy/WfKgcJyka1bugqsqBN/zYDaY4+bKeRwcb/GcNwAWWZMRNxcWzBdDo6+aYYEEuoPPfxfr4n4v1YBogGxChStBOPq1zRHhWX53ak70+Q/Cw7NwQstH8wPsXvOqNX1NbkSXvquwabUyDXDcula1ing54jVax0sp+yHU7x3ccrU00YvFgXFg02WqYP/OjOayP0BvHSc7+V6Se2vi3QrpB12ojiqwMonl4rHhpoNx1za6Sl0xJw5KN64RUJhfNKpEZpduzuaOoZ4RM4pXntmtzwgyrIcvJ62ZCgKx4ojxx7Yc/GHdpKH4hPnVOqIIDd4g29pdKuxhxuy/0Ws0OL8Vs6z0FZFqipKjMPAuWwK1xzW8sSHS/198Vm92TuXyQzf9uVJLVo3mKfbMZIt3789m5sJvUnDECL6gED2g7WXdkUg9Oio8ePnYrD+q5+CLYB7lwD+MqE0ls2+G+s4NgkOX3aB9umn2rzs41b5QKlQgvIql6nZrYrWKtoGqa6kGwNVyJos6w6jDze619QVhWUILFVceB6ek4fpP0zOL+vjAPekg1WslS9ryOrcMr3gBJXNNHnDn637cbZz8U4PgDY0mNtY/tdfDqwLCPP1QE748tLCXTEjNAnh/e/rCdA15IoaWHyGSvuHIqrWsEGBzukqPq+BaJJD62W1EOQs+/O71SxxolQaZ6T8hcJLOkD9JexvJgCiWVSpms0IQDUBuxd4QeD32gXbAGxjIk2qVqd53QkVTYevDIPNXIeo2eDTwyqgAttdY30AB1yRQy6xKte0HswUYSfXGfdP1zwJUb/7Ft0k3BCq8Q79kv9pc7GS9SofupbuktNy4r+LmA==

I am trying to understand the error message “A module cannot be applied to another module application or with-_expression_”.

The minimal example:

Module Type CType.  Parameter Inline t : Type. End CType.
Module CNat <: CType. Definition t := nat. End CNat.
Module Type M (Import CT: CType). End M.
Module Z (Import MN: M CNat). End Z.

Fail Module Import ZMN := Z(M(CNat)).
(*
The command has indeed failed with message:

A module cannot be applied to another module application or with-_expression_; you must
give a name to the intermediate result module first.
*)

Module Type MN := M(CNat).
Fail Module Import ZMN := Z(MN).
(*
The command has indeed failed with message:

Illegal application to a module type.
*)

What would be the proper way to do something like this?

Thanks!

—
Vadim Zaliva
CMU ECE Ph.D. candidate
Mobile/Signal/WhatsApp: +1(510)220-1060

[Coq-Club] A module cannot be applied to another module application or with-expression, Vadim Zaliva, 11/22/2019
- Re: [Coq-Club] A module cannot be applied to another module application or with-expression, Vadim Zaliva, 11/22/2019
  - Re: [Coq-Club] A module cannot be applied to another module application or with-expression, Pierre Courtieu, 11/22/2019
- Re: [Coq-Club] A module cannot be applied to another module application or with-expression, Pierre Courtieu, 11/22/2019