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