Nuprl Definition : prior-as-rec-bind-class2
prior-as-rec-bind-class2(X) ==
on-first-class(Lift(X)) >>= rec-bind-class(λi.prior-as-rec-bind-class-out2(i);λi.prior-as-rec-bind-class-in2(X;i))
Definitions occuring in Statement :
prior-as-rec-bind-class-in2: prior-as-rec-bind-class-in2(X;i),
prior-as-rec-bind-class-out2: prior-as-rec-bind-class-out2(i),
rec-bind-class: rec-bind-class(X;Y),
on-first-class: on-first-class(X),
lift-class: Lift(X),
mbind-class: X >>= Y,
lambda: λx.A[x]
FDL editor aliases :
prior-as-rec-bind-class2
Latex:
prior-as-rec-bind-class2(X) ==
on-first-class(Lift(X)) >>= rec-bind-class(\mlambda{}i.prior-as-rec-bind-class-out2(i);\mlambda{}i....)
Date html generated:
2015_07_21-PM-03_15_29
Last ObjectModification:
2012_04_17-AM-00_45_58
Home
Index