Nuprl Definition : p-first

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


Definitions occuring in Statement :  list_accum: list_accum,  it: ⋅,  apply: f a,  lambda: λx.A[x],  decide: case b of inl(x) => s[x] | inr(y) => t[y],  inr: inr x 
Definitions occuring in definition :  lambda: λx.A[x],  list_accum: list_accum,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  apply: f a,  inr: inr x ,  it: ⋅
FDL editor aliases :  p-first
Latex:
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:
              L
          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