Nuprl Definition : find
(first x ∈ as s.t. P[x] else d) == case filter(λx.P[x];as) of [] => d | a::b => a esac
Definitions occuring in Statement :
filter: filter(P;l),
list_ind: list_ind,
lambda: λx.A[x]
Definitions occuring in definition :
list_ind: list_ind,
filter: filter(P;l),
lambda: λx.A[x]
FDL editor aliases :
find
Latex:
(first x \mmember{} as s.t. P[x] else d) == case filter(\mlambda{}x.P[x];as) of [] => d | a::b => a esac
Date html generated:
2016_05_15-PM-01_54_37
Last ObjectModification:
2015_09_23-AM-07_37_24
Theory : list!
Home
Index