Nuprl Definition : term-ind

term-ind(x.varcase[x];f,bts,r.mktermcase[f;
                                         bts;
                                         r];t) ==
  letrec P(a)=case a
   of inl(x) =>
   varcase[x]
   | inr(p) =>
   let f,bts = p 
   in mktermcase[f;
                 bts;
                 λi.(P (snd(bts[i])))] in
   P(t)


Definitions occuring in Statement :  select: L[n],  genrec-ap: genrec-ap,  pi2: snd(t),  apply: f a,  lambda: λx.A[x],  spread: spread def,  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],  apply: f a,  pi2: snd(t),  select: L[n]
FDL editor aliases :  term-ind
Latex:
term-ind(x.varcase[x];f,bts,r.mktermcase[f;
                                                                                  bts;
                                                                                  r];t)  ==
    letrec  P(a)=case  a
      of  inl(x)  =>
      varcase[x]
      |  inr(p)  =>
      let  f,bts  =  p 
      in  mktermcase[f;
                                  bts;
                                  \mlambda{}i.(P  (snd(bts[i])))]  in
      P(t)


Date html generated: 2020_05_19-PM-09_54_25
Last ObjectModification: 2020_03_09-PM-04_08_34

Theory : terms


Home Index