I'm generally confused about the module system, but specifically confused about the following point. I have a module type foo
containing a parameter declaration, and a module myfoo : foo
instantiating that parameter with a definition. However, when I try to use anything from myfoo
, it behaves as if no instantiation actually happened. The definition does not compute to its own body, and printing the definition prints something weird. If I remove the : foo
type annotation, things work as I'd expect. What's going on here, and why?
Module Type foo.
Parameter n : nat.
End foo.
Module myfoo : foo.
Definition n := 3.
End myfoo.
Eval cbv in myfoo.n.
(* = myfoo.n
* : nat
*)
Print myfoo.n.
(* *** [ myfoo.n : nat ] *)
Goal myfoo.n = 3.
Fail reflexivity.
The type annotation indeed seals the module. If you just want to check the type without sealing you can do <: foo
.
Aha, I'd seen that syntactic form in the documentation, but thought that the only difference was whether the interface was restricted to just the parameters of the module type. I guess the mnemonic here is that :
restricts the entire observable behaviour of the module to what is specified by the module type, right?
Yeah that sounds right.
Thanks :smiley:
James Wood has marked this topic as resolved.
Incidentally, if someone is looking for some documentation to improve, The Module System would be a good one to do, in my opinion. I'd be willing to discuss my problems with it.
Last updated: Oct 13 2024 at 01:02 UTC