Nuprl Definition : p-first

p-first(L) ==
  λx.accumulate (with value and list item f):
      case of inl(z) => inr(z) => x
     over list:
     with starting value:
      inr ⋅ )

Definitions occuring in Statement :  list_accum: list_accum it: apply: a lambda: λx.A[x] decide: case of inl(x) => s[x] inr(y) => t[y] inr: inr 
Definitions occuring in definition :  lambda: λx.A[x] list_accum: list_accum decide: case of inl(x) => s[x] inr(y) => t[y] apply: a inr: inr  it:
FDL editor aliases :  p-first

p-first(L)  ==
    \mlambda{}x.accumulate  (with  value  v  and  list  item  f):
            case  v  of  inl(z)  =>  v  |  inr(z)  =>  f  x
          over  list:
          with  starting  value:
            inr  \mcdot{}  )

Date html generated: 2016_05_15-PM-03_30_11
Last ObjectModification: 2015_09_23-AM-07_43_48

Theory : general

Home Index