Possible Error On Page 63

[Joseph]

Page 63 defines the following type rule for modules:

pi --> D: pi_1 dec
------------------------------
pi --> module I = {D}:{I:pi_1}dec

However, this contradicts the type rule from page 58:
pi --> D: pi_1 dec
------------------------------
pi --> module I = {D}:{I:pi_1 dec}dec

The difference being that there is an extra dec in the module's type. I
believe that the second should be used, otherwise, whatever is defined
inside the module would become available without an import.

Anyone have thoughts?

Cheers,
Joseph

[Joseph]

Post by Joseph
pi --> D: pi_1 dec
------------------------------
pi --> module I = {D}:{I:pi_1}dec
pi --> D: pi_1 dec
------------------------------
pi --> module I = {D}:{I:pi_1 dec}dec
The difference being that there is an extra dec in the module's type. I
believe that the second should be used, otherwise, whatever is defined
inside the module would become available without an import.
Anyone have thoughts?
Cheers,
Joseph

Never mind, I think the rules from page 63 are fine. I think I
overreacted to the inconsistency between page 63 and page 58.