Nuprl Definition : rec-op-bind-class
rec-op-bind-class(X;Y;F) == fix((λrec-op-bind-class,v. X v || Y v >>= λu,es,e. (F u (rec-op-bind-class u es e))))
Definitions occuring in Statement :
mbind-class: X >>= Y,
parallel-class: X || Y,
apply: f a,
fix: fix(F),
lambda: λx.A[x]
FDL editor aliases :
rec-op-bind-class
Latex:
rec-op-bind-class(X;Y;F) ==
fix((\mlambda{}rec-op-bind-class,v. X v || Y v >>= \mlambda{}u,es,e. (F u (rec-op-bind-class u es e))))
Date html generated:
2015_07_21-PM-03_16_12
Last ObjectModification:
2012_07_02-PM-04_13_08
Home
Index