Nuprl Definition : term-accum

term-accum(t with parm)
p,f,vs,tr.Q[p;
            f;
            vs;
            tr]
varterm(v) with p ⇒ varcase[p; v]
mkterm(f,bts) with p ⇒ trs.mktermcase[p;
                                       f;
                                       bts;
                                       trs] ==
  term-accum1(t)
  p,f,vs,tr.Q[p;
              f;
              vs;
              tr]
  varterm(v) with p ⇒ varcase[p; v]
  mkterm(f,bts) with p ⇒ trs.mktermcase[p;
                                         f;
                                         bts;
                                         trs]
  parm

Definitions occuring in Statement : term-accum1: term-accum1, apply: f a
Definitions occuring in definition : apply: f a, term-accum1: term-accum1
FDL editor aliases : term-accum

Latex:
term-accum(t with parm) p,f,vs,tr.Q[p; f; vs; tr] varterm(v) with p {}\mRightarrow{} varcase[p; v] mkterm(f,bts) with p {}\mRightarrow{} trs.mktermcase[p; f; bts; trs] == term-accum1(t) p,f,vs,tr.Q[p; f; vs; tr] varterm(v) with p {}\mRightarrow{} varcase[p; v] mkterm(f,bts) with p {}\mRightarrow{} trs.mktermcase[p; f; bts; trs] parm Date html generated: 2020_05_19-PM-09_55_11 Last ObjectModification: 2020_03_09-PM-04_08_44 Theory : terms Home Index