[[P |- module I={D}: {I:P1dec}dec]]e s = ({I=e1}, s1) where (e1, s1) = [[P |- D: P1dec]]e s [[P |- import I: P1dec]]e s = (e1, s) where (I=e1) in e
Eager evaluation allocates storage when module is defined.