Nuprl Definition : pairs-fpf
fpf(L) ==
<remove-repeats(eq1;map(λp.(fst(p));L)), λx.reduce(λp,l. if eqof(eq1) (fst(p)) x then insert(snd(p);l) else l fi ;[];L\000C)>
Definitions occuring in Statement :
remove-repeats: remove-repeats(eq;L),
insert: insert(a;L),
map: map(f;as),
reduce: reduce(f;k;as),
nil: [],
eqof: eqof(d),
ifthenelse: if b then t else f fi ,
pi1: fst(t),
pi2: snd(t),
apply: f a,
lambda: λx.A[x],
pair: <a, b>
FDL editor aliases :
pairs-fpf
Latex:
fpf(L) ==
<remove-repeats(eq1;map(\mlambda{}p.(fst(p));L))
, \mlambda{}x.reduce(\mlambda{}p,l. if eqof(eq1) (fst(p)) x then insert(snd(p);l) else l fi ;[];L)
>
Date html generated:
2016_05_16-AM-11_36_35
Last ObjectModification:
2012_02_25-AM-11_14_29
Theory : event-ordering
Home
Index