Nuprl Definition : ml-list-delete

ml-list-delete(as;i) ==
  fix((λlistdel,as,i. if null(as)
                     then []
                     else let a.more = as 
                          in if i <z 1 then more else [a / listdel(more)(i - 1)] fi 
                     fi ))(as)(i)


Definitions occuring in Statement :  spreadcons: spreadcons,  ml_apply: f(x),  null: null(as),  cons: [a / b],  nil: [],  ifthenelse: if b then t else f fi ,  lt_int: i <z j,  fix: fix(F),  lambda: λx.A[x],  subtract: n - m,  natural_number: $n
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  null: null(as),  nil: [],  spreadcons: spreadcons,  ifthenelse: if b then t else f fi ,  lt_int: i <z j,  cons: [a / b],  ml_apply: f(x),  subtract: n - m,  natural_number: $n
FDL editor aliases :  ml-list-delete
Latex:
ml-list-delete(as;i)  ==
    fix((\mlambda{}listdel,as,i.  if  null(as)
                                          then  []
                                          else  let  a.more  =  as 
                                                    in  if  i  <z  1  then  more  else  [a  /  listdel(more)(i  -  1)]  fi 
                                          fi  ))(as)(i)


Date html generated: 2017_09_29-PM-05_56_58
Last ObjectModification: 2017_05_19-PM-06_05_20

Theory : omega


Home Index