Nuprl Definition : pv11_p1_CommanderState

pv11_p1_CommanderState(Cmd;accpts;mf) ==  λb,s. state-class1(λloc.accpts;pv11_p1_on_p2b() b s;pv11_p1_p2b'base(Cmd;mf))


Definitions occuring in Statement :  pv11_p1_on_p2b: pv11_p1_on_p2b(),  pv11_p1_p2b'base: pv11_p1_p2b'base(Cmd;mf),  state-class1: state-class1(init;tr;X),  apply: f a,  lambda: λx.A[x]
FDL editor aliases :  pv11_p1_CommanderState
Latex:
pv11\_p1\_CommanderState(Cmd;accpts;mf)  ==
    \mlambda{}b,s.  state-class1(\mlambda{}loc.accpts;pv11\_p1\_on\_p2b()  b  s;pv11\_p1\_p2b'base(Cmd;mf))


Date html generated: 2015_07_23-PM-04_13_25
Last ObjectModification: 2014_11_26-AM-11_26_49

Home Index