Nuprl Definition : l-first

l-first(x.f[x];L) ==  rec-case(L) of [] => inr x.Ax)  x::xs => r.if f[x] then inl else fi 

Definitions occuring in Statement :  list_ind: list_ind ifthenelse: if then else fi  lambda: λx.A[x] inr: inr  inl: inl x axiom: Ax
Definitions occuring in definition :  list_ind: list_ind inr: inr  lambda: λx.A[x] axiom: Ax ifthenelse: if then else fi  inl: inl x
FDL editor aliases :  l-first

l-first(x.f[x];L)  ==    rec-case(L)  of  []  =>  inr  (\mlambda{}x.Ax)    |  x::xs  =>  r.if  f[x]  then  inl  x  else  r  fi 

Date html generated: 2016_05_14-AM-07_48_10
Last ObjectModification: 2015_09_22-PM-05_54_01

Theory : list_1

Home Index