Nuprl Definition : until-class
(X until Y) == λes,e. case class-pred(Y;es;e) of inl(e') => {} | inr(z) => X es e
Definitions occuring in Statement :
class-pred: class-pred(X;es;e),
apply: f a,
lambda: λx.A[x],
decide: case b of inl(x) => s[x] | inr(y) => t[y],
empty-bag: {}
FDL editor aliases :
until-class
Latex:
(X until Y) == \mlambda{}es,e. case class-pred(Y;es;e) of inl(e') => \{\} | inr(z) => X es e
Date html generated:
2015_07_20-PM-03_58_28
Last ObjectModification:
2012_02_25-PM-01_59_38
Home
Index