Nuprl Definition : invert-union
invert-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 :
invert-union
Latex:
invert-union(x) == case x of inl(a) => inr a | inr(a) => inl a
Date html generated:
2016_05_15-PM-03_26_54
Last ObjectModification:
2015_09_23-AM-07_43_23
Theory : general
Home
Index