Nuprl Definition : lg-append
lg-append(g1;g2) ==
g1 @ map(λtr.let lbl,in,out = tr in <lbl, map(λx.(x + lg-size(g1));in), map(λx.(x + lg-size(g1));out)>;g2)
Definitions occuring in Statement :
lg-size: lg-size(g),
map: map(f;as),
append: as @ bs,
spreadn: spread3,
lambda: λx.A[x],
pair: <a, b>,
add: n + m
FDL editor aliases :
lg-append
Latex:
lg-append(g1;g2) ==
g1
@ map(\mlambda{}tr.let lbl,in,out = tr in
<lbl, map(\mlambda{}x.(x + lg-size(g1));in), map(\mlambda{}x.(x + lg-size(g1));out)>g2)
Date html generated:
2015_07_22-PM-00_27_38
Last ObjectModification:
2012_02_25-PM-03_33_44
Home
Index