Nuprl Definition : threshold_accum
threshold_accum(test;
nxt;
step;
g) ==
λp,x. if test (fst(p)) x then <nxt <fst(p), x>, g <fst(p), x>> else <step (fst(p)) x, ff> fi
Definitions occuring in Statement :
ifthenelse: if b then t else f fi ,
bfalse: ff,
pi1: fst(t),
apply: f a,
lambda: λx.A[x],
pair: <a, b>
FDL editor aliases :
threshold_accum
threshold_accum
threshold\_accum(test;
nxt;
step;
g) ==
\mlambda{}p,x. if test (fst(p)) x then <nxt <fst(p), x>, g <fst(p), x>> else <step (fst(p)) x, ff> fi
Date html generated:
2015_07_17-AM-08_58_58
Last ObjectModification:
2013_03_25-PM-01_54_40
Home
Index