Nuprl Definition : st-lookup
st-lookup(tab;x) ==
let K,p,f = tab in
let n = mu(λn.(p <z n ∨bK ≤z n ∨bfst((f n)) =a1 x)) in
if p <z n ∨bK ≤z n then inr ⋅ else inl (snd((f n))) fi
Definitions occuring in Statement :
mu: mu(f),
le_int: i ≤z j,
bor: p ∨bq,
eq_atom: eq_atom$n(x;y),
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
let: let,
it: ⋅,
spreadn: spread3,
pi1: fst(t),
pi2: snd(t),
apply: f a,
lambda: λx.A[x],
inr: inr x ,
inl: inl x
FDL editor aliases :
st-lookup
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:
2015_07_17-AM-08_56_00
Last ObjectModification:
2013_03_25-PM-01_53_07
Home
Index