Nuprl Definition : list-partition

list-partition(f;L) ==
  rec-case(L) of
  [] => <[], []>
  a::as =>
   r.let left,right = r
     in if f ||as|| then <[a / left], right> else <left, [a / right]> fi

Definitions occuring in Statement : length: ||as||, list_ind: list_ind, cons: [a / b], nil: [], ifthenelse: if b then t else f fi , apply: f a, spread: spread def, pair: <a, b>
Definitions occuring in definition : list_ind: list_ind, nil: [], spread: spread def, ifthenelse: if b then t else f fi , apply: f a, length: ||as||, pair: <a, b>, cons: [a / b]
FDL editor aliases : list-partition

Latex:
list-partition(f;L) == rec-case(L) of [] => <[], []> a::as => r.let left,right = r in if f ||as|| then <[a / left], right> else <left, [a / right]> fi Date html generated: 2016_05_14-PM-03_18_30 Last ObjectModification: 2015_09_22-PM-05_59_20 Theory : list_1 Home Index