Nuprl Definition : hered-term-accum

hered-term-accum(par,vars,v.varcase[par;
                                    vars;
                                    v];
                 prm,vs,f,L.m[prm;
                              vs;
                              f;
                              L];
                 p0,ws,op,sofar,bt.param[p0;
                                         ws;
                                         op;
                                         sofar;
                                         bt];
                 param;
                 bndtrm) ==
  let vs,t = bndtrm
  in case t
      of inl(v) =>
      varcase[param;
              vs;
              v]
      | inr(pr) =>
      let f,bts = pr
      in let L = bound-terms-accum(sofar,bt.param[param;
                                                  vs;
                                                  f;
                                                  sofar;

                                                  bt];p',bt.hered-term-accum(par,vars,v.varcase[par;

                                                                                                vars;

v];

                                                                             prm,vs,f,L.m[prm;

vs;

f;

L];

                                                                             p0,ws,op,sofar,bt.param[p0;

ws;

op;

                                                                                                     sofar;

                                                                                                     bt];

p';

                                                                             bt);bts) in

             m[param;
               vs;
               f;
               L]

Definitions occuring in Statement : bound-terms-accum: bound-terms-accum(L,bt.f[L; bt];param,bndtrm.g[param; bndtrm];bts), let: let, spread: spread def, decide: case b of inl(x) => s[x] | inr(y) => t[y]
Definitions occuring in definition : decide: case b of inl(x) => s[x] | inr(y) => t[y], spread: spread def, let: let, bound-terms-accum: bound-terms-accum(L,bt.f[L; bt];param,bndtrm.g[param; bndtrm];bts)
FDL editor aliases : hered-term-accum

Latex:
hered-term-accum(par,vars,v.varcase[par; vars; v]; prm,vs,f,L.m[prm; vs; f; L]; p0,ws,op,sofar,bt.param[p0; ws; op; sofar; bt]; param; bndtrm) == let vs,t = bndtrm in case t of inl(v) => varcase[param; vs; v] | inr(pr) => let f,bts = pr in let L = bound-terms-accum(sofar,bt.param[param; vs; f; sofar; bt];p',bt.hered-term-accum (par,vars,v.varcase[par; vars; v]; prm,vs,f,L.m[prm; vs; f; L]; p0,ws,op,sofar,bt.param[p0; ws; op; sofar; bt]; p'; bt);bts) in m[param; vs; f; L] Date html generated: 2020_05_19-PM-09_54_45 Last ObjectModification: 2020_03_09-PM-06_30_04 Theory : terms Home Index