Nuprl Definition : oob-apply
oob-apply(xs;ys) ==
if (#(xs) =z 1) then if (#(ys) =z 1) then {oobboth(<only(xs), only(ys)>)} else {oobleft(only(xs))} fi
if (#(ys) =z 1) then {oobright(only(ys))}
else {}
fi
Definitions occuring in Statement :
oobright: oobright(rval),
oobleft: oobleft(lval),
oobboth: oobboth(bval),
bag-only: only(bs),
bag-size: #(bs),
single-bag: {x},
empty-bag: {},
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
pair: <a, b>,
natural_number: $n
Definitions occuring in definition :
oobboth: oobboth(bval),
pair: <a, b>,
oobleft: oobleft(lval),
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
bag-size: #(bs),
natural_number: $n,
single-bag: {x},
oobright: oobright(rval),
bag-only: only(bs),
empty-bag: {}
FDL editor aliases :
oob-apply
Latex:
oob-apply(xs;ys) ==
if (\#(xs) =\msubz{} 1) then if (\#(ys) =\msubz{} 1) then \{oobboth(<only(xs), only(ys)>)\} else \{oobleft(only(xs))\}\000C fi
if (\#(ys) =\msubz{} 1) then \{oobright(only(ys))\}
else \{\}
fi
Date html generated:
2016_05_15-PM-07_33_52
Last ObjectModification:
2015_09_23-AM-08_16_44
Theory : general
Home
Index