Nuprl Definition : ci-port
ci-port(l;tg;T) ==
mk_ci(es-decl-set-single(destination(l);⊗;rcv(l,tg) : T);T;λx.let i,k,s,v = x
in if k = rcv(l,tg) then inl v else inr ⋅ fi )
Definitions occuring in Statement :
mk_ci: mk_ci(dd;T;f),
ifthenelse: if b then t else f fi ,
it: ⋅,
lambda: λx.A[x],
inr: inr x ,
inl: inl x
FDL editor aliases :
ci-port
ci-port
ci-port(l;tg;T) ==
mk\_ci(es-decl-set-single(destination(l);\motimes{};rcv(l,tg) : T);T;\mlambda{}x.let i,k,s,v = x
in if k = rcv(l,tg)
then inl v
else inr \mcdot{}
fi )
Date html generated:
2015_07_17-AM-08_57_59
Last ObjectModification:
2013_03_25-PM-01_54_11
Home
Index