Nuprl Definition : p-co-filter
p-co-filter(f) == λx.case f x of inl(p) => inr p | inr(p) => inl x
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,
inr: inr x ,
inl: inl x
FDL editor aliases :
p-co-filter
Latex:
p-co-filter(f) == \mlambda{}x.case f x of inl(p) => inr p | inr(p) => inl x
Date html generated:
2016_05_15-PM-03_30_47
Last ObjectModification:
2015_09_23-AM-07_43_54
Theory : general
Home
Index