Nuprl Definition : bs_tree_lookup
bs_tree_lookup(cmp;x;tr) ==
case(tr)
null=>inr ⋅
leaf(v)=>if (cmp v x =z 0) then inl v else inr ⋅ fi
node(a,v,b)=>la,lb.eval c = cmp v x in
if (c) < (0) then la else if (0) < (c) then lb else (inl v)
Definitions occuring in Statement :
bs_tree_ind: bs_tree_ind,
callbyvalue: callbyvalue,
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
it: ⋅,
less: if (a) < (b) then c else d,
apply: f a,
inr: inr x ,
inl: inl x,
natural_number: $n
Definitions occuring in definition :
bs_tree_ind: bs_tree_ind,
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
inr: inr x ,
it: ⋅,
callbyvalue: callbyvalue,
apply: f a,
less: if (a) < (b) then c else d,
natural_number: $n,
inl: inl x
FDL editor aliases :
bs_tree_lookup
Latex:
bs\_tree\_lookup(cmp;x;tr) ==
case(tr)
null=>inr \mcdot{}
leaf(v)=>if (cmp v x =\msubz{} 0) then inl v else inr \mcdot{} fi
node(a,v,b)=>la,lb.eval c = cmp v x in
if (c) < (0) then la else if (0) < (c) then lb else (inl v)
Date html generated:
2016_05_15-PM-01_52_53
Last ObjectModification:
2016_04_08-PM-06_21_49
Theory : tree_1
Home
Index