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