Nuprl Definition : modify-combinator2

modify-combinator2(f) ==
  λu,p. (f u 
         (λi.if (i =z 0)
               then case p 0 of inl(xy) => if oob-hasleft(xy) then inl oob-getleft(xy) else ff fi  | inr(_) => ff
             if (i =z 1)
               then case p 0 of inl(xy) => if oob-hasright(xy) then inl oob-getright(xy) else ff fi  | inr(_) => ff
             else p (i - 1)
             fi ))


Definitions occuring in Statement :  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  bfalse: ff,  apply: f a,  lambda: λx.A[x],  decide: case b of inl(x) => s[x] | inr(y) => t[y],  inl: inl x,  subtract: n - m,  natural_number: $n,  oob-getright: oob-getright(x),  oob-hasright: oob-hasright(x),  oob-getleft: oob-getleft(x),  oob-hasleft: oob-hasleft(x)
FDL editor aliases :  modify-combinator2 modify-combinator2
modify-combinator2(f)  ==
    \mlambda{}u,p.  (f  u 
                  (\mlambda{}i.if  (i  =\msubz{}  0)
                              then  case  p  0
                                          of  inl(xy)  =>
                                          if  oob-hasleft(xy)  then  inl  oob-getleft(xy)  else  ff  fi 
                                          |  inr($_{}$)  =>
                                          ff
                          if  (i  =\msubz{}  1)
                              then  case  p  0
                                          of  inl(xy)  =>
                                          if  oob-hasright(xy)  then  inl  oob-getright(xy)  else  ff  fi 
                                          |  inr($_{}$)  =>
                                          ff
                          else  p  (i  -  1)
                          fi  ))


Date html generated: 2015_07_17-AM-08_59_33
Last ObjectModification: 2013_03_25-PM-01_54_55

Home Index