Nuprl Definition : collect_filter_accum_fun

collect_filter_accum_fun(b,v.f[b; v];base;size;v.num[v];v.P[v]) ==
  λs,v. eval n = num[v] in
        eval vok = P[v] in
          let i,m,b,w = s 
          in if n <z i then <i, m, b, inr 0 >
             if vok
               then if i <z n
                    then if (1 =z size) then <n + 1, 0, f[base; v], inl tt> else <n, 1, f[base; v], inr 0 > fi 
                    else eval m' = m + 1 in
                         if (m' =z size) then <i + 1, 0, f[base; v], inl tt> else <i, m', f[b; v], inr 0 > fi 
                    fi 
             if i <z n then <n + 1, 0, f[base; v], inl ff>
             else <i + 1, 0, f[b; v], inl ff>
             fi   


Definitions occuring in Statement :  callbyvalue: callbyvalue,  ifthenelse: if b then t else f fi ,  lt_int: i <z j,  eq_int: (i =z j),  bfalse: ff,  btrue: tt,  spreadn: spread4,  lambda: λx.A[x],  pair: <a, b>,  inr: inr x ,  inl: inl x,  add: n + m,  natural_number: $n
FDL editor aliases :  collect_filter_accum_fun collect_filter_accum_fun
collect\_filter\_accum\_fun(b,v.f[b;  v];base;size;v.num[v];v.P[v])  ==
    \mlambda{}s,v.  eval  n  =  num[v]  in
                eval  vok  =  P[v]  in
                    let  i,m,b,w  =  s 
                    in  if  n  <z  i  then  <i,  m,  b,  inr  0  >
                          if  vok
                              then  if  i  <z  n
                                        then  if  (1  =\msubz{}  size)
                                                  then  <n  +  1,  0,  f[base;  v],  inl  tt>
                                                  else  <n,  1,  f[base;  v],  inr  0  >
                                                  fi 
                                        else  eval  m'  =  m  +  1  in
                                                  if  (m'  =\msubz{}  size)
                                                  then  <i  +  1,  0,  f[base;  v],  inl  tt>
                                                  else  <i,  m',  f[b;  v],  inr  0  >
                                                  fi 
                                        fi 
                          if  i  <z  n  then  <n  +  1,  0,  f[base;  v],  inl  ff>
                          else  <i  +  1,  0,  f[b;  v],  inl  ff>
                          fi     


Date html generated: 2015_07_17-AM-09_00_16
Last ObjectModification: 2013_03_25-PM-01_55_06

Home Index