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 x else r fi
Definitions occuring in Statement :
list_ind: list_ind,
ifthenelse: if b then t else f fi ,
lambda: λx.A[x],
inr: inr x ,
inl: inl x,
axiom: Ax
Definitions occuring in definition :
list_ind: list_ind,
inr: inr x ,
lambda: λx.A[x],
axiom: Ax,
ifthenelse: if b then t else f fi ,
inl: inl x
FDL editor aliases :
l-first
Latex:
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