Nuprl Definition : system-fpf
system-fpf(S) ==
let Cs,G = S
in let dom = remove-repeats(IdDeq;map(λp.(fst(p));Cs) @ map(λnd.(snd(fst(fst(nd))));G)) in
mkfpf(dom;λx.<mapfilter(λc.(snd(c));λc.fst(c) = x;Cs), lg-filter(λtr.snd(fst(tr)) = x;G)>)
Definitions occuring in Statement :
lg-filter: lg-filter(P;G),
mkfpf: mkfpf(a;b),
eq_id: a = b,
id-deq: IdDeq,
remove-repeats: remove-repeats(eq;L),
mapfilter: mapfilter(f;P;L),
map: map(f;as),
append: as @ bs,
let: let,
pi1: fst(t),
pi2: snd(t),
lambda: λx.A[x],
spread: spread def,
pair: <a, b>
FDL editor aliases :
system-fpf
Latex:
system-fpf(S) ==
let Cs,G = S
in let dom = remove-repeats(IdDeq;map(\mlambda{}p.(fst(p));Cs) @ map(\mlambda{}nd.(snd(fst(fst(nd))));G)) in
mkfpf(dom;\mlambda{}x.<mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c) = x;Cs), lg-filter(\mlambda{}tr.snd(fst(tr)) = x;G)>)
Date html generated:
2015_07_23-AM-11_08_19
Last ObjectModification:
2012_02_25-PM-03_39_04
Home
Index