Nuprl Definition : l_find
l_find(L;P) == reduce(λh,r. if P h then inl h else r fi ;inr ⋅ ;L)
Definitions occuring in Statement :
reduce: reduce(f;k;as),
ifthenelse: if b then t else f fi ,
it: ⋅,
apply: f a,
lambda: λx.A[x],
inr: inr x ,
inl: inl x
Definitions occuring in definition :
reduce: reduce(f;k;as),
lambda: λx.A[x],
ifthenelse: if b then t else f fi ,
apply: f a,
inl: inl x,
inr: inr x ,
it: ⋅
FDL editor aliases :
l_find
Latex:
l\_find(L;P) == reduce(\mlambda{}h,r. if P h then inl h else r fi ;inr \mcdot{} ;L)
Date html generated:
2016_05_15-PM-03_39_28
Last ObjectModification:
2015_09_23-AM-07_44_31
Theory : general
Home
Index