Nuprl Definition : fpf-normalize
fpf-normalize(eq;g) == reduce(λx,f. x : (snd(g)) x ⊕ f;⊗;fst(g))
Definitions occuring in Statement :
fpf-single: x : v,
fpf-join: f ⊕ g,
fpf-empty: ⊗,
reduce: reduce(f;k;as),
pi1: fst(t),
pi2: snd(t),
apply: f a,
lambda: λx.A[x]
FDL editor aliases :
fpf-normalize
fpf-normalize(eq;g) == reduce(\mlambda{}x,f. x : (snd(g)) x \moplus{} f;\motimes{};fst(g))
Date html generated:
2015_07_17-AM-11_16_40
Last ObjectModification:
2012_02_25-AM-11_14_37
Home
Index