The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

Ok, I was not aware of the Import feature. I still find it a weird place to have it, as it can be mistaken with what I thought it was.
I do not have Coq under my hand here, so I cannot test if "Module Import. End Import." is also rejected, but I guess it is.

The Coq site seems down for now, but as far as I remember, there is a 'with' annotation for module types which can be useful for you (read the documentation on modules when documentation becomes available back).
Clearly in your original example, at no point you made it clear to Coq that in your Implementation module, "ht = list …". You may not require to put it in your A module but in this case as Beta said, but in this case you will probably need to use intermediate parametric modules.

I also suggest to take a look on Record/Class alternatives. In Ocaml and many other languages, types are not first class citizens, so you need stuff like modules to manipulate them. In Coq, types are regular values, so you can put them inside of regular records, and I find it often a lot more convenient than using the module mechanism, and I find it also a lot easier to learn/read/write/understand. (Still there are cases where you do not have much choice, e.g. when you want to use a Coq library using modules.)

2014-06-13 1:16 GMT+02:00 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?

Yes, that is what I meant, but the remaining part of your mail shows me that I was wrong.
 

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

--
.../Sedrikov\...