Nuprl Definition : next
(next i > k s.t. ↑p[i]) == fix((λnext,k. eval j = k + 1 in if p[j] then j else next j fi )) k
Definitions occuring in Statement :
callbyvalue: callbyvalue,
ifthenelse: if b then t else f fi ,
apply: f a,
fix: fix(F),
lambda: λx.A[x],
add: n + m,
natural_number: $n
Definitions occuring in definition :
fix: fix(F),
lambda: λx.A[x],
callbyvalue: callbyvalue,
add: n + m,
natural_number: $n,
ifthenelse: if b then t else f fi ,
apply: f a
FDL editor aliases :
next
Latex:
(next i > k s.t. \muparrow{}p[i]) == fix((\mlambda{}next,k. eval j = k + 1 in if p[j] then j else next j fi )) k
Date html generated:
2016_05_15-PM-03_59_44
Last ObjectModification:
2015_09_23-AM-07_45_52
Theory : general
Home
Index