Go backward to Indexing of Module Components Go up to Top Go forward to Redeclaration of Modules |
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 };
in call M.INIT; call N.SUCC