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