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:
2020_05_20-AM-08_59_03
Last ObjectModification:
2017_01_23-PM-10_15_28
Theory : lattices
Home
Index