st-lookup(tab;x) ==
let K,p,f = tab in
let n = mu(
n.(p <z n 
K 
z n fst((f n)) =a1 x)) in
if p <z n K z n then inr 
else inl (snd((f n))) fi
Definitions :
spreadn: spread3,
let: let,
mu: mu(f),
lambda: x.A[x],
eq_atom: eq_atom$n(x;y),
pi1: fst(t),
ifthenelse: if b then t else f fi ,
bor: p q,
lt_int: i <z j,
le_int: i z j,
inr: inr x ,
it: ,
inl: inl x ,
pi2: snd(t),
apply: f a
FDL editor aliases :
st-lookup
st-lookup(tab;x) ==
let K,p,f = tab in
let n = mu(\mlambda{}n.(p <z n \mvee{}\msubb{}K \mleq{}z n \mvee{}\msubb{}fst((f n)) =a1 x)) in
if p <z n \mvee{}\msubb{}K \mleq{}z n then inr \mcdot{} else inl (snd((f n))) fi
Date html generated:
2010_08_27-AM-09_33_59
Last ObjectModification:
2009_12_16-AM-01_14_49
Home
Index