Nuprl Definition : mu_ex_v4_State
mu_ex_v4_State(initial_token) ==
SM4-class-du(mu_ex_v4_initState(initial_token);<mu_ex_v4_onRequest(), mu_ex_v4_Request()>;<mu_ex_v4_onToken()
, mu_ex_v4_Token()
>;<mu_ex_v4_onUseCS(), mu_ex_v4_UseCS()>;<mu_ex_v4_onLeaveCS(), mu_ex_v4_LeaveCS()>)
Definitions occuring in Statement :
mu_ex_v4_initState: mu_ex_v4_initState(initial_token),
mu_ex_v4_onLeaveCS: mu_ex_v4_onLeaveCS(),
mu_ex_v4_onUseCS: mu_ex_v4_onUseCS(),
mu_ex_v4_onToken: mu_ex_v4_onToken(),
mu_ex_v4_onRequest: mu_ex_v4_onRequest(),
mu_ex_v4_UseCS: mu_ex_v4_UseCS(),
mu_ex_v4_LeaveCS: mu_ex_v4_LeaveCS(),
mu_ex_v4_Token: mu_ex_v4_Token(),
mu_ex_v4_Request: mu_ex_v4_Request(),
SM4-class-du: SM4-class-du(init;trX1;trX2;trX3;trX4),
pair: <a, b>
FDL editor aliases :
mu_ex_v4_State
mu\_ex\_v4\_State(initial$_{token}$) ==
SM4-class-du(mu\_ex\_v4\_initState(initial$_{token}$);<mu\_ex\_v4\_onRequest()
, mu\_ex\_v4\_Request()
><mu\_ex\_v4\_onToken(), mu\_ex\_v4\_Token()><mu\_ex\_v4\_onUseCS()
, mu\_ex\_v4\_UseCS()
><mu\_ex\_v4\_onLeaveCS(), mu\_ex\_v4\_LeaveCS()>)
Date html generated:
2012_02_20-PM-06_30_50
Last ObjectModification:
2012_02_02-PM-02_52_54
Home
Index