Nuprl Definition : p-filter
p-filter(f) == λx.case f x of inl(p) => inl x | inr(p) => inr p
Definitions occuring in Statement :
apply: f a,
lambda: λx.A[x],
decide: case b of inl(x) => s[x] | inr(y) => t[y],
inr: inr x ,
inl: inl x
Definitions occuring in definition :
lambda: λx.A[x],
decide: case b of inl(x) => s[x] | inr(y) => t[y],
apply: f a,
inl: inl x,
inr: inr x
FDL editor aliases :
p-filter
Latex:
p-filter(f) == \mlambda{}x.case f x of inl(p) => inl x | inr(p) => inr p
Date html generated:
2016_05_15-PM-03_30_42
Last ObjectModification:
2015_09_23-AM-07_43_52
Theory : general
Home
Index