Nuprl Definition : one_or_both_ind
one_or_both_ind(x;bval.both[bval];lval.left[lval];rval.right[rval]) ==
case x of inl(x) => both[x] | inr(x) => case x of inl(x) => left[x] | inr(x) => right[x]
Definitions occuring in Statement :
decide: case b of inl(x) => s[x] | inr(y) => t[y]
Definitions occuring in definition :
decide: case b of inl(x) => s[x] | inr(y) => t[y]
FDL editor aliases :
one_or_both_ind
Latex:
one\_or\_both\_ind(x;bval.both[bval];lval.left[lval];rval.right[rval]) ==
case x of inl(x) => both[x] | inr(x) => case x of inl(x) => left[x] | inr(x) => right[x]
Date html generated:
2016_05_15-PM-05_32_23
Last ObjectModification:
2015_09_23-AM-07_55_42
Theory : general
Home
Index