Nuprl Definition : oarcast-deliver-output
oarcast-deliver-output(num;s) ==
let rem,counts = s
in eval L = eval_list(mapfilter(λp.(fst(p));λp.num ≤z snd(p);counts)) in
if null(L) then inr ⋅ else let xx,_ = L in inl xx fi
Definitions occuring in Statement :
mapfilter: mapfilter(f;P;L),
null: null(as),
eval_list: eval_list(t),
le_int: i ≤z j,
callbyvalue: callbyvalue,
ifthenelse: if b then t else f fi ,
it: ⋅,
pi1: fst(t),
pi2: snd(t),
lambda: λx.A[x],
spread: spread def,
inr: inr x ,
inl: inl x
FDL editor aliases :
oarcast-deliver-output
Latex:
oarcast-deliver-output(num;s) ==
let rem,counts = s
in eval L = eval\_list(mapfilter(\mlambda{}p.(fst(p));\mlambda{}p.num \mleq{}z snd(p);counts)) in
if null(L) then inr \mcdot{} else let xx,$_{}$ = L in inl xx fi
Date html generated:
2016_05_17-PM-00_57_47
Last ObjectModification:
2014_07_23-PM-01_27_45
Theory : event-logic-applications
Home
Index