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)
, 
eqof: eqof(d)
, 
map: map(f;as)
, 
reduce: reduce(f;k;as)
, 
nil: []
, 
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
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:
2015_07_17-AM-11_16_24
Last ObjectModification:
2012_02_25-AM-11_14_29
Home
Index