x:Id, k:Knd, A,T:Type, f:(ATA). ma-single-effect0(x;A;k;T;f)  MsgA

1

1. x : Id 2. k : Knd 3. A : Type 4. T : Type 5. f : ATA   (s,v. f(s(x),v))  State(x : A)ma-valtype(k : T; k)x : A(x)?Void

8 steps

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html