Nuprl Definition : list-delete

as\i==r if as = Ax then as otherwise let a,as2 = as in if (i) < (1)  then as2  else [a / as2\i - 1]
as\i ==
  fix((λlist-delete,as,i. if as = Ax then as otherwise let a,as2 = as 
                                                       in if (i) < (1)  then as2  else [a / (list-delete as2 (i - 1))]))\000C 
  as 
  i


Definitions occuring in Statement :  cons: [a / b],  isaxiom: if z = Ax then a otherwise b,  less: if (a) < (b)  then c  else d,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  spread: spread def,  subtract: n - m,  natural_number: $n
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  isaxiom: if z = Ax then a otherwise b,  spread: spread def,  less: if (a) < (b)  then c  else d,  cons: [a / b],  apply: f a,  subtract: n - m,  natural_number: $n
FDL editor aliases :  list-delete
Latex:
as\mbackslash{}i==r  if  as  =  Ax  then  as  otherwise  let  a,as2  =  as  in  if  (i)  <  (1)    then  as2    else  [a  /  as2\mbackslash{}i  -  1]
Latex:
as\mbackslash{}i  ==
    fix((\mlambda{}list-delete,as,i.  if  as  =  Ax  then  as  otherwise  let  a,as2  =  as 
                                                                                                              in  if  (i)  <  (1)
                                                                                                                          then  as2
                                                                                                                          else  [a  /  (list-delete  as2  (i  -  1))])) 
    as 
    i


Date html generated: 2016_05_14-AM-06_56_20
Last ObjectModification: 2015_09_22-PM-05_51_17

Theory : omega


Home Index