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>
Definitions occuring in definition :
pair: <a, b>,
remove-repeats: remove-repeats(eq;L),
map: map(f;as),
reduce: reduce(f;k;as),
lambda: λx.A[x],
ifthenelse: if b then t else f fi ,
apply: f a,
eqof: eqof(d),
pi1: fst(t),
insert: insert(a;L),
pi2: snd(t),
nil: []
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:
2018_05_21-PM-09_31_47
Last ObjectModification:
2018_02_09-AM-10_26_41
Theory : finite!partial!functions
Home
Index