Nuprl Definition : reject

as\[i] ==
  fix((λreject,i,as. if i ≤then tl(as) else case as of [] => [] a'::as' => [a' (reject (i 1) as')] esac fi )) \000Ci as

Definitions occuring in Statement :  tl: tl(l) list_ind: list_ind cons: [a b] nil: [] le_int: i ≤j ifthenelse: if then else fi  apply: a fix: fix(F) lambda: λx.A[x] subtract: m natural_number: $n
Definitions occuring in definition :  fix: fix(F) lambda: λx.A[x] ifthenelse: if then else fi  le_int: i ≤j tl: tl(l) list_ind: list_ind nil: [] cons: [a b] apply: a subtract: m natural_number: $n
FDL editor aliases :  reject

as\mbackslash{}[i]  ==
    fix((\mlambda{}reject,i,as.  if  i  \mleq{}z  0
                                        then  tl(as)
                                        else  case  as  of  []  =>  []  |  a'::as'  =>  [a'  /  (reject  (i  -  1)  as')]  esac
                                        fi  )) 

Date html generated: 2016_05_14-AM-06_28_43
Last ObjectModification: 2015_12_03-PM-02_05_51

Theory : list_0

Home Index