The Coq mailing list

[Christopher Ernest Sally <christopherernestsally AT gmail.com>]

Hi Cedric

Oh, you mean like forall (x y : nat) etc etc? Then both x and y are nats?

I don't quite understand how Import works, but if I run this script

Module Type A.
Parameter a : Type.
End A.

Module Type B (T: A).
  Check T.a.
  (*Check Import.a. *) (* Error: The reference Import.a was not found in the current environment. *)

  (*Parameter x : a.*)(*Error: The reference a was not found in the current environment.*)
End B.  Print Module Type B.

Module Type C (Import T: A).
  Parameter x : a.
End C.  Print Module Type C.

Module Type D (Import : A). (*Gives an error. Seems "Import" is reserved *)

"Import" as a module doesn't seem to show up in C. And while one can "Check" T.a in both B & C, you can only use it in C.

What I meant in the previous email is that the import would allow us to have the variables, k v and m, which would serve as abstract types for Interface', but still allow us to make them concrete later in Interface. (but _how_ that works, I'm not sure)

Warm regards
Chris