Nuprl Definition : baseof
baseof(T) == ⋂x:Unit?. case x of inl(z) => T | inr(z) => Base
Definitions occuring in Statement :
unit: Unit,
isect: ⋂x:A. B[x],
decide: case b 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 b of inl(x) => s[x] | inr(y) => t[y],
base: Base
FDL editor aliases :
baseof
Latex:
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