Nuprl Definition : term-accum1

term-accum1(t)
p,f,vs,L.Q[p;
           f;
           vs;
           L]
varterm(v) with p ⇒ varcase[p; v]
mkterm(f,bts) with p ⇒ trs.mktermcase[p;
                                       f;
                                       bts;
                                       trs] ==
  letrec R(a)=case a
   of inl(v) =>
   λp.varcase[p; v]
   | inr(pr) =>
   let f,bts = pr 
   in λp.let trs = accumulate (with value L and list item bt):
                    let p' = Q[p;
                               f;
                               fst(bt);
                               L] in
                        L @ [<snd(bt), p', R (snd(bt)) p'>]
                   over list:
                     bts
                   with starting value:
                    []) in
             mktermcase[p;
                        f;
                        bts;
                        trs] in
   R(t)


Definitions occuring in Statement :  append: as @ bs,  list_accum: list_accum,  cons: [a / b],  nil: [],  genrec-ap: genrec-ap,  let: let,  pi1: fst(t),  pi2: snd(t),  apply: f a,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  decide: case b of inl(x) => s[x] | inr(y) => t[y]
Definitions occuring in definition :  genrec-ap: genrec-ap,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  spread: spread def,  lambda: λx.A[x],  list_accum: list_accum,  let: let,  pi1: fst(t),  append: as @ bs,  cons: [a / b],  pair: <a, b>,  apply: f a,  pi2: snd(t),  nil: []
FDL editor aliases :  term-accum1
Latex:
term-accum1(t)
p,f,vs,L.Q[p;
                      f;
                      vs;
                      L]
varterm(v)  with  p  {}\mRightarrow{}  varcase[p;  v]
mkterm(f,bts)  with  p  {}\mRightarrow{}  trs.mktermcase[p;
                                                                              f;
                                                                              bts;
                                                                              trs]  ==
    letrec  R(a)=case  a
      of  inl(v)  =>
      \mlambda{}p.varcase[p;  v]
      |  inr(pr)  =>
      let  f,bts  =  pr 
      in  \mlambda{}p.let  trs  =  accumulate  (with  value  L  and  list  item  bt):
                                        let  p'  =  Q[p;
                                                              f;
                                                              fst(bt);
                                                              L]  in
                                                L  @  [<snd(bt),  p',  R  (snd(bt))  p'>]
                                      over  list:
                                          bts
                                      with  starting  value:
                                        [])  in
                          mktermcase[p;
                                                f;
                                                bts;
                                                trs]  in
      R(t)


Date html generated: 2020_05_19-PM-09_55_04
Last ObjectModification: 2020_03_09-PM-04_08_40

Theory : terms


Home Index