Nuprl Definition : flip-union
flip-union(x) ==  case x of inl(a) => inr a  | inr(a) => inl a
Definitions occuring in Statement : 
decide: case b of inl(x) => s[x] | inr(y) => t[y]
, 
inr: inr x 
, 
inl: inl x
Definitions occuring in definition : 
decide: case b of inl(x) => s[x] | inr(y) => t[y]
, 
inr: inr x 
, 
inl: inl x
FDL editor aliases : 
flip-union
Latex:
flip-union(x)  ==    case  x  of  inl(a)  =>  inr  a    |  inr(a)  =>  inl  a
Date html generated:
2017_02_21-AM-09_57_12
Last ObjectModification:
2017_01_23-PM-10_15_28
Theory : lattices
Home
Index