Nuprl Definition : boot-process
boot-process(f;n) ==
RecProcess(inr ⋅ ;s,m.case s
of inl(P) =>
let Q,e = P m
in <inl Q, e>
| inr(x) =>
case f m of inl(P) => <inl P, n> | inr(x) => <s, n>)
Definitions occuring in Statement :
rec-process: RecProcess(s0;s,m.next[s; m]),
it: ⋅,
apply: f a,
spread: spread def,
pair: <a, b>,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
inr: inr x ,
inl: inl x
FDL editor aliases :
boot-process
boot-process(f;n) ==
RecProcess(inr \mcdot{} ;s,m.case s
of inl(P) =>
let Q,e = P m
in <inl Q, e>
| inr(x) =>
case f m of inl(P) => <inl P, n> | inr(x) => <s, n>)
Date html generated:
2015_07_17-AM-11_20_22
Last ObjectModification:
2012_02_25-AM-11_38_44
Home
Index