Nuprl Definition : un-zip
un-zip(as) == reduce(λa,p. let p1,p2 = p in let a1,a2 = a in <[a1 / p1], [a2 / p2]>;<[], []>;as)
Definitions occuring in Statement :
reduce: reduce(f;k;as),
cons: [a / b],
nil: [],
lambda: λx.A[x],
spread: spread def,
pair: <a, b>
Definitions occuring in definition :
reduce: reduce(f;k;as),
lambda: λx.A[x],
spread: spread def,
cons: [a / b],
pair: <a, b>,
nil: []
FDL editor aliases :
un-zip
Latex:
un-zip(as) == reduce(\mlambda{}a,p. let p1,p2 = p in let a1,a2 = a in <[a1 / p1], [a2 / p2]><[], []>as)
Date html generated:
2016_05_15-PM-03_57_48
Last ObjectModification:
2015_09_23-AM-07_45_43
Theory : general
Home
Index