Nuprl Definition : prior-as-rec-bind-class

prior-as-rec-bind-class(X) ==
rec-bind-class(λi.prior-as-rec-bind-class-out(i);λi.prior-as-rec-bind-class-in(X;i)) (inr inr ⋅ )

Definitions occuring in Statement : prior-as-rec-bind-class-in: prior-as-rec-bind-class-in(X;i), prior-as-rec-bind-class-out: prior-as-rec-bind-class-out(i), rec-bind-class: rec-bind-class(X;Y), it: ⋅, apply: f a, lambda: λx.A[x], inr: inr x
FDL editor aliases : prior-as-rec-bind-class

Latex:
prior-as-rec-bind-class(X) == rec-bind-class(\mlambda{}i.prior-as-rec-bind-class-out(i);\mlambda{}i.prior-as-rec-bind-class-in(X;i)) (inr inr \mcdot{} ) Date html generated: 2015_07_21-PM-03_14_14 Last ObjectModification: 2012_04_15-AM-02_29_13 Home Index