Nuprl Definition : modify-combinator1

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



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



Date html generated: 2015_07_17-AM-08_59_26
Last ObjectModification: 2013_03_25-PM-01_54_52

Home Index