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
Latex:
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:
2016_05_16-AM-10_00_33
Last ObjectModification:
2013_03_25-PM-01_53_07
Theory : new!event-ordering
Home
Index