Nuprl Definition : ci-or
ci1 | ci2 ==
let dd1,A,f = ci1 in
let dd2,B,g = ci2 in
mk_ci(es-decl-set-join(dd1;dd2);one_or_both(A;B);λx.oob-apply(λx.if es-info-loc(x) ∈b |dd1|
∧b es-info-kind(x) ∈ dom(da(dd1;es-info-loc(x)))
then f x
else inr ⋅
fi ;
λx.if es-info-loc(x) ∈b |dd2|
∧b es-info-kind(x) ∈ dom(da(dd2;es-info-loc(x)))
then g x
else inr ⋅
fi ;
x))
Definitions occuring in Statement :
mk_ci: mk_ci(dd;T;f),
id-deq: IdDeq,
deq-member: x ∈b L,
band: p ∧b q,
ifthenelse: if b then t else f fi ,
it: ⋅,
spreadn: spread3,
apply: f a,
lambda: λx.A[x],
inr: inr x ,
one_or_both: one_or_both(A;B)
FDL editor aliases :
ci-or
ci-or
Latex:
ci1 | ci2 ==
let dd1,A,f = ci1 in
let dd2,B,g = ci2 in
mk\_ci(es-decl-set-join(dd1;dd2);one\_or\_both(A;B);
\mlambda{}x.oob-apply(\mlambda{}x.if es-info-loc(x) \mmember{}\msubb{} |dd1| \mwedge{}\msubb{} es-info-kind(x) \mmember{} dom(da(dd1;es-info-loc(x)))
then f x
else inr \mcdot{}
fi ;
\mlambda{}x.if es-info-loc(x) \mmember{}\msubb{} |dd2| \mwedge{}\msubb{} es-info-kind(x) \mmember{} dom(da(dd2;es-info-loc(x)))
then g x
else inr \mcdot{}
fi ;
x))
Date html generated:
2016_05_16-AM-10_05_50
Last ObjectModification:
2013_03_25-PM-01_54_13
Theory : new!event-ordering
Home
Index