Nuprl Definition : type2tree

type2tree(A;B;C) ==  W(C A; of inl(n) => Void inr(m) => B)

Definitions occuring in Statement :  W: W(A;a.B[a]) decide: case 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 of inl(x) => s[x] inr(y) => t[y] void: Void
FDL editor aliases :  type2tree

type2tree(A;B;C)  ==    W(C  +  A;  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