Nuprl Definition : oob-getleft
oob-getleft(x) == if oobleft?(x) then oobleft-lval(x) else fst(oobboth-bval(x)) fi
Definitions occuring in Statement :
oobleft-lval: oobleft-lval(x)
,
oobleft?: oobleft?(x)
,
oobboth-bval: oobboth-bval(x)
,
ifthenelse: if b then t else f fi
,
pi1: fst(t)
Definitions occuring in definition :
ifthenelse: if b then t else f fi
,
oobleft?: oobleft?(x)
,
oobleft-lval: oobleft-lval(x)
,
pi1: fst(t)
,
oobboth-bval: oobboth-bval(x)
FDL editor aliases :
oob-getleft
Latex:
oob-getleft(x) == if oobleft?(x) then oobleft-lval(x) else fst(oobboth-bval(x)) fi
Date html generated:
2016_05_15-PM-05_35_45
Last ObjectModification:
2015_09_23-AM-07_56_47
Theory : general
Home
Index