Nuprl Definition : split_tail

split_tail(L | ∀x.f[x]) ==
  fix((λsplit_tail,L. case L of 
                        [] => <[], []> 
                        a::as =>
                         let hs,ftail = split_tail as 
                         in case hs of 
                              [] => if f[a] then <[], [a / ftail]> else <[a], ftail> fi  
                              x::y =>
                               <[a / hs], ftail> 
                            esac 
                     esac)) 
  L


Definitions occuring in Statement :  list_ind: list_ind,  cons: [a / b],  nil: [],  ifthenelse: if b then t else f fi ,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  spread: spread def,  pair: <a, b>
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  spread: spread def,  apply: f a,  list_ind: list_ind,  ifthenelse: if b then t else f fi ,  nil: [],  pair: <a, b>,  cons: [a / b]
FDL editor aliases :  split_tail
Latex:
split\_tail(L  |  \mforall{}x.f[x])  ==
    fix((\mlambda{}split$_{tail}$,L.  case  L  of 
                                              []  =>  <[],  []> 
                                              a::as  =>
                                                let  hs,ftail  =  split$_{tail}$  as 
                                                in  case  hs  of 
                                                          []  =>  if  f[a]  then  <[],  [a  /  ftail]>  else  <[a],  ftail>  fi   
                                                          x::y  =>
                                                            <[a  /  hs],  ftail> 
                                                      esac 
                                        esac)) 
    L


Date html generated: 2016_05_15-PM-01_56_00
Last ObjectModification: 2015_09_23-AM-07_37_30

Theory : list!


Home Index