The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

Maybe I should explain better where this is coming from. The problem I am trying to solve is that I end up with two instances of the same module which are distinct as shown in the snippet below. So I am trying to see if I can instantiate it once and pass around to other modules as in my original example.

Module Type CType. Parameter Inline t : Type. End CType.
Module CNat <: CType. Definition t := nat. End CNat.
Module M (Import CT: CType).
  Definition fst: t. Admitted.
End M.
Print M.

Module M1 := M(CNat).
Module M2 := M(CNat).

Goal M1.fst = M2.fst.
Proof.
  Fail reflexivity.
  (*
    The command has indeed failed with message:
    Unable to unify "M2.fst" with "M1.fst".
   *)
Qed.

Vadim

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

On Thu, Nov 21, 2019 at 7:47 PM Vadim Zaliva <vzaliva AT cmu.edu> wrote:

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