Nuprl Definition : sbdecode
sbdecode(L) == reduce(λx,p. let m,n = p in if x=0 then <m, m + n> else <m + n, n>;<1, 1>;L)
Definitions occuring in Statement :
reduce: reduce(f;k;as),
int_eq: if a=b then c else d,
lambda: λx.A[x],
spread: spread def,
pair: <a, b>,
add: n + m,
natural_number: $n
Definitions occuring in definition :
reduce: reduce(f;k;as),
lambda: λx.A[x],
spread: spread def,
int_eq: if a=b then c else d,
add: n + m,
pair: <a, b>,
natural_number: $n
FDL editor aliases :
sbdecode
Latex:
sbdecode(L) == reduce(\mlambda{}x,p. let m,n = p in if x=0 then <m, m + n> else <m + n, n>ə, 1>L)
Date html generated:
2016_05_15-PM-10_34_12
Last ObjectModification:
2015_09_23-AM-08_26_48
Theory : rationals
Home
Index