Nuprl Definition : vr_upd_lst_ks

vr_upd_lst_ks(i;lst) ==
  let b,lst = vr_foldl(elt,y.
                        let b,lst = y 
                        in if b
                           then if elt <z i then <ff, lst @ [elt + 1]> else <tt, lst @ [0]> fi 
                           else <ff, lst @ [elt]>
                           fi ;<tt, []>;lst) 
  in if b then lst @ [1] else lst fi 


Definitions occuring in Statement :  vr_foldl: vr_foldl(f;a;lst),  append: as @ bs,  lt_int: i <z j,  ifthenelse: if b then t else f fi ,  bfalse: ff,  btrue: tt,  lambda: x.A[x],  spread: spread def,  pair: <a, b>,  cons: [car / cdr],  nil: [],  add: n + m,  natural_number: $n
FDL editor aliases :  vr_upd_lst_ks
vr\_upd\_lst\_ks(i;lst)  ==
    let  b,lst  =  vr\_foldl(\mlambda{}elt,y.
                                                let  b,lst  =  y 
                                                in  if  b
                                                      then  if  elt  <z  i  then  <ff,  lst  @  [elt  +  1]>  else  <tt,  lst  @  [0]>  fi 
                                                      else  <ff,  lst  @  [elt]>
                                                      fi  ;<tt,  []>lst) 
    in  if  b  then  lst  @  [1]  else  lst  fi 


Date html generated: 2012_02_20-PM-03_30_49
Last ObjectModification: 2012_02_02-PM-01_54_44

Home Index