Nuprl Definition : type2tree
type2tree(A;B;C) == W(C + A;d.case d of inl(n) => Void | inr(m) => B)
Definitions occuring in Statement :
W: W(A;a.B[a]),
decide: case b of inl(x) => s[x] | inr(y) => t[y],
union: left + right,
void: Void
Definitions occuring in definition :
W: W(A;a.B[a]),
union: left + right,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
void: Void
FDL editor aliases :
type2tree
Latex:
type2tree(A;B;C) == W(C + A;d.case d of inl(n) => Void | inr(m) => B)
Date html generated:
2019_06_20-PM-03_08_13
Last ObjectModification:
2018_08_13-AM-11_43_18
Theory : continuity
Home
Index