---

inning_step() ==
  s,x.
   let vs,i = s in
     case x
    of inl(v) => s
     | inr(p) => let j,v = p in
                   if (j = i - 1) then <[v / vs], i> else s fi 

---

Definitions :  lambda: x.A[x],  decide: case b of inl(x) => s[x] | inr(y) => t[y],  spread: spread def,  ifthenelse: if b then t else f fi ,  eq_int: (i = j),  subtract: n - m,  natural_number: $n,  pair: <a, b>,  cons: [car / cdr]
FDL editor aliases :  inning_step

---

inning\_step()  ==
    \mlambda{}s,x.
      let  vs,i  =  s  in
          case  x  of  inl(v)  =>  s  |  inr(p)  =>  let  j,v  =  p  in  if  (j  =\msubz{}  i  -  1)  then  <[v  /  vs],  i>  else  s  fi 


Date html generated: 2010_08_27-PM-08_30_30
Last ObjectModification: 2010_06_23-PM-11_56_33

Home Index