Nuprl Definition : first-success

first-success(f;L) ==
  rec-case(L) of
  [] => inr ⋅ 
  a::as =>
   r.case f a of inl(x) => inl <0, x> | inr(_) => case r of inl(p) => let i,x = p in inl <i + 1, x> | inr(z) => inr z 


Definitions occuring in Statement :  list_ind: list_ind,  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,  add: n + m,  natural_number: $n
Definitions occuring in definition :  list_ind: list_ind,  it: ⋅,  apply: f a,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  spread: spread def,  inl: inl x,  pair: <a, b>,  add: n + m,  natural_number: $n,  inr: inr x 
FDL editor aliases :  first-success
Latex:
first-success(f;L)  ==
    rec-case(L)  of
    []  =>  inr  \mcdot{} 
    a::as  =>
      r.case  f  a
      of  inl(x)  =>
      inl  ɘ,  x>
      |  inr($_{}$)  =>
      case  r  of  inl(p)  =>  let  i,x  =  p  in  inl  <i  +  1,  x>  |  inr(z)  =>  inr  z 


Date html generated: 2016_05_14-AM-06_37_06
Last ObjectModification: 2015_12_03-PM-02_08_03

Theory : list_0


Home Index