Nuprl Definition : lg-remove
lg-remove(g;n) ==
map(λtr.let lbl,in,out = tr in
<lbl
, map(λx.if x ≤z n then x else x - 1 fi ;filter(λx.(¬b(x =z n));in))
, map(λx.if x ≤z n then x else x - 1 fi ;filter(λx.(¬b(x =z n));out))>;firstn(n;g) @ nth_tl(n + 1;g))
Definitions occuring in Statement :
filter: filter(P;l),
firstn: firstn(n;as),
nth_tl: nth_tl(n;as),
map: map(f;as),
append: as @ bs,
le_int: i ≤z j,
bnot: ¬bb,
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
spreadn: spread3,
lambda: λx.A[x],
pair: <a, b>,
subtract: n - m,
add: n + m,
natural_number: $n
FDL editor aliases :
lg-remove
Latex:
lg-remove(g;n) ==
map(\mlambda{}tr.let lbl,in,out = tr in
<lbl
, map(\mlambda{}x.if x \mleq{}z n then x else x - 1 fi ;filter(\mlambda{}x.(\mneg{}\msubb{}(x =\msubz{} n));in))
, map(\mlambda{}x.if x \mleq{}z n then x else x - 1 fi ;filter(\mlambda{}x.(\mneg{}\msubb{}(x =\msubz{} n));out))>firstn(n;g)
@ nth\_tl(n + 1;g))
Date html generated:
2015_07_22-PM-00_28_08
Last ObjectModification:
2012_02_25-PM-03_34_11
Home
Index