Nuprl Definition : dcdr-to-bool
[d]b == case d of inl(x) => inl ⋅ | inr(x) => inr ⋅
Definitions occuring in Statement :
it: ⋅,
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],
inl: inl x,
inr: inr x ,
it: ⋅
FDL editor aliases :
dcdr-to-bool
Latex:
[d]\msubb{} == case d of inl(x) => inl \mcdot{} | inr(x) => inr \mcdot{}
Date html generated:
2016_05_13-PM-03_58_20
Last ObjectModification:
2015_09_22-PM-05_45_41
Theory : bool_1
Home
Index