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
Latex:
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: 2016_05_16-AM-10_05_43
Last ObjectModification: 2013_03_25-PM-01_54_11

Theory : new!event-ordering


Home Index