Nuprl Definition : reject
as\[i] ==
fix((λreject,i,as. if i ≤z 0 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 ≤z j,
ifthenelse: if b then t else f fi ,
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],
ifthenelse: if b then t else f fi ,
le_int: i ≤z j,
tl: tl(l),
list_ind: list_ind,
nil: [],
cons: [a / b],
apply: f a,
subtract: n - m,
natural_number: $n
FDL editor aliases :
reject
Latex:
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 ))
i
as
Date html generated:
2016_05_14-AM-06_28_43
Last ObjectModification:
2015_12_03-PM-02_05_51
Theory : list_0
Home
Index