Nuprl Definition : repeat-on-success

repeat-on-success(f;g;h;as;b)
==r case first-success(f;as)
     of inl(v) =>
     eval as' = evalall(g v as) in
     eval b' = h v b in
       repeat-on-success(f;g;h;as';b')
     | inr(_) =>
     <as, b>

repeat-on-success(f;g;h;as;b) ==
  fix((λrepeat-on-success,as,b. case first-success(f;as)
                                of inl(v) =>
                                eval as' = evalall(g v as) in
                                eval b' = h v b in
                                  repeat-on-success as' b'
                                | inr(_) =>
                                <as, b>))
  as
  b

Definitions occuring in Statement : first-success: first-success(f;L), evalall: evalall(t), callbyvalue: callbyvalue, apply: f a, fix: fix(F), lambda: λx.A[x], pair: <a, b>, decide: case b of inl(x) => s[x] | inr(y) => t[y]
Definitions occuring in definition : fix: fix(F), lambda: λx.A[x], decide: case b of inl(x) => s[x] | inr(y) => t[y], first-success: first-success(f;L), evalall: evalall(t), callbyvalue: callbyvalue, apply: f a, pair: <a, b>
FDL editor aliases : repeat-on-success

Latex:
repeat-on-success(f;g;h;as;b) ==r case first-success(f;as) of inl(v) => eval as' = evalall(g v as) in eval b' = h v b in repeat-on-success(f;g;h;as';b') | inr($_{}$) => <as, b>

Latex:
repeat-on-success(f;g;h;as;b) == fix((\mlambda{}repeat-on-success,as,b. case first-success(f;as) of inl(v) => eval as' = evalall(g v as) in eval b' = h v b in repeat-on-success as' b' | inr($_{}$) => <as, b>)) as b Date html generated: 2016_05_14-AM-06_39_02 Last ObjectModification: 2015_12_03-PM-02_08_07 Theory : list_0 Home Index