Nuprl Definition : baseof

baseof(T) ==  ⋂x:Unit?. case of inl(z) => inr(z) => Base

Definitions occuring in Statement :  unit: Unit isect: x:A. B[x] decide: case of inl(x) => s[x] inr(y) => t[y] union: left right base: Base
Definitions occuring in definition :  isect: x:A. B[x] union: left right unit: Unit decide: case of inl(x) => s[x] inr(y) => t[y] base: Base
FDL editor aliases :  baseof

baseof(T)  ==    \mcap{}x:Unit?.  case  x  of  inl(z)  =>  T  |  inr(z)  =>  Base

Date html generated: 2016_05_13-PM-03_16_03
Last ObjectModification: 2016_01_04-AM-10_26_46

Theory : core_2

Home Index