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
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:
2015_07_17-AM-08_58_02
Last ObjectModification:
2013_03_25-PM-01_54_13
Home
Index