Nuprl Definition : add-sz

add-sz(sz;L;x) ==
  tuple-sum(λc,u. case c of inl(z) => case z of inl(p) => sz p u | inr(p) => l_sum(map(sz p;u)) | inr(E) => 0;L;x)


Definitions occuring in Statement :  tuple-sum: tuple-sum(f;L;x),  l_sum: l_sum(L),  map: map(f;as),  apply: f a,  lambda: λx.A[x],  decide: case b of inl(x) => s[x] | inr(y) => t[y],  natural_number: $n
Definitions occuring in definition :  tuple-sum: tuple-sum(f;L;x),  lambda: λx.A[x],  decide: case b of inl(x) => s[x] | inr(y) => t[y],  l_sum: l_sum(L),  map: map(f;as),  apply: f a,  natural_number: $n
FDL editor aliases :  add-sz
Latex:
add-sz(sz;L;x)  ==
    tuple-sum(\mlambda{}c,u.  case  c
                                    of  inl(z)  =>
                                    case  z  of  inl(p)  =>  sz  p  u  |  inr(p)  =>  l\_sum(map(sz  p;u))
                                    |  inr(E)  =>
                                    0;L;x)


Date html generated: 2019_06_20-PM-02_04_11
Last ObjectModification: 2019_02_22-AM-11_16_31

Theory : tuples


Home Index