Nuprl Definition : select-indices-aux
select-indices-aux(f;L) ==
rec-case(L) of
[] => λn.[]
fst::rest =>
r.if f fst then λn.[n / (r (n + 1))] else λn.(r (n + 1)) fi
Definitions occuring in Statement :
list_ind: list_ind,
cons: [a / b],
nil: [],
ifthenelse: if b then t else f fi ,
apply: f a,
lambda: λx.A[x],
add: n + m,
natural_number: $n
FDL editor aliases :
select-indices-aux
Latex:
select-indices-aux(f;L) ==
rec-case(L) of
[] => \mlambda{}n.[]
fst::rest =>
r.if f fst then \mlambda{}n.[n / (r (n + 1))] else \mlambda{}n.(r (n + 1)) fi
Date html generated:
2015_07_23-AM-11_59_53
Last ObjectModification:
2012_08_30-PM-01_51_28
Home
Index