module S = { var A: K; fun
F=@A+1 };
module M = { import S; proc
INIT=A:=0 };
module N = { import S; proc
SUCC=A:=F };
import M; import N;
in call INIT; call SUCC
- Prohibited by typing rules.
- S would be imported twice!
- However, makes sense if S is evaluated eagerly!
Alternative typing rules required for eagerly evaluated modules and
multiple import of same module.
