Nuprl Definition : es-dt
dt(l;da) ==
compose-fpf(λk.if isrcv(k) then if lnk(k) = l then inl tag(k) else inr ⋅ fi else inr ⋅ fi ;λtg.rcv(l,tg);da)
Definitions occuring in Statement :
compose-fpf: compose-fpf(a;b;f),
eq_lnk: a = b,
tagof: tag(k),
lnk: lnk(k),
rcv: rcv(l,tg),
isrcv: isrcv(k),
ifthenelse: if b then t else f fi ,
it: ⋅,
lambda: λx.A[x],
inr: inr x ,
inl: inl x
FDL editor aliases :
es-dt
dt(l;da) ==
compose-fpf(...;\mlambda{}tg.rcv(l,tg);da)
Date html generated:
2015_07_17-AM-11_17_46
Last ObjectModification:
2012_02_25-AM-11_15_16
Home
Index