Nuprl Definition : compose-tuple-recodings
r2 o r1 == λL1.let L2,h1,j1 = r1 L1 in let L3,h2,j2 = r2 L2 in <L3, h2 o h1, j1 o j2>
Definitions occuring in Statement :
compose: f o g,
spreadn: spread3,
apply: f a,
lambda: λx.A[x],
pair: <a, b>
Definitions occuring in definition :
lambda: λx.A[x],
spreadn: spread3,
apply: f a,
pair: <a, b>,
compose: f o g
FDL editor aliases :
compose-tuple-recodings
Latex:
r2 o r1 == \mlambda{}L1.let L2,h1,j1 = r1 L1 in let L3,h2,j2 = r2 L2 in <L3, h2 o h1, j1 o j2>
Date html generated:
2016_05_15-PM-05_49_53
Last ObjectModification:
2015_09_23-AM-07_59_26
Theory : general
Home
Index