Nuprl Definition : firstn

firstn(n;as) ==
  fix((λfirstn,n,as. case as of [] => [] | a::as' => if 0 <z n then [a / (firstn (n - 1) as')] else [] fi  esac)) n as


Definitions occuring in Statement :  list_ind: list_ind,  cons: [a / b],  nil: [],  ifthenelse: if b then t else f fi ,  lt_int: i <z j,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  subtract: n - m,  natural_number: $n
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  list_ind: list_ind,  ifthenelse: if b then t else f fi ,  lt_int: i <z j,  cons: [a / b],  apply: f a,  subtract: n - m,  natural_number: $n,  nil: []
FDL editor aliases :  firstn
Latex:
firstn(n;as)  ==
    fix((\mlambda{}firstn,n,as.  case  as  of 
                                              []  =>  [] 
                                              a::as'  =>
                                                if  0  <z  n  then  [a  /  (firstn  (n  -  1)  as')]  else  []  fi   
                                        esac)) 
    n 
    as


Date html generated: 2016_05_14-AM-06_47_50
Last ObjectModification: 2015_12_03-PM-02_05_42

Theory : list_0


Home Index