Nuprl Definition : add-graph-decls
add-graph-decls(dd;G;T;a;b) == let S,ds,da = dd in <S, ds, λi.graph-rcvs(S;G;a;b;i) |-fpf-> T ⊕ da i>
Definitions occuring in Statement :
fpf-const: L |-fpf-> v,
fpf-join: f ⊕ g,
graph-rcvs: graph-rcvs(S;G;a;b;j),
Kind-deq: KindDeq,
spreadn: spread3,
apply: f a,
lambda: λx.A[x],
pair: <a, b>
FDL editor aliases :
add-graph-decls
Latex:
add-graph-decls(dd;G;T;a;b) ==
let S,ds,da = dd in
<S, ds, \mlambda{}i.graph-rcvs(S;G;a;b;i) |-fpf-> T \moplus{} da i>
Date html generated:
2016_05_16-PM-00_58_41
Last ObjectModification:
2013_03_27-AM-11_08_48
Theory : event-ordering
Home
Index