---

modify-combinator2(f) ==
  u,p.
   (f u 
    (i.if (i = 0)
          then case p 0
               of inl(xy) => if oob-hasleft(xy)
                             then inl oob-getleft(xy) 
                             else ff
                             fi 
                | inr(_) => ff
        if (i = 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 :  lambda: x.A[x],  oob-hasleft: oob-hasleft(x),  oob-getleft: oob-getleft(x),  eq_int: (i = j),  decide: case b of inl(x) => s[x] | inr(y) => t[y],  ifthenelse: if b then t else f fi ,  oob-hasright: oob-hasright(x),  inl: inl x ,  oob-getright: oob-getright(x),  bfalse: ff,  apply: f a,  subtract: n - m,  natural_number: $n
FDL editor aliases :  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: 2010_08_27-AM-09_37_09
Last ObjectModification: 2009_12_16-AM-08_34_43

Home Index