Nuprl Definition : tag-case
z:T == x:Atom × if x =a z then T else Top fi
Definitions occuring in Statement :
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
top: Top,
product: x:A × B[x],
atom: Atom
Definitions occuring in definition :
product: x:A × B[x],
atom: Atom,
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
top: Top
FDL editor aliases :
tag-case
Latex:
z:T == x:Atom \mtimes{} if x =a z then T else Top fi
Date html generated:
2016_05_15-PM-06_43_37
Last ObjectModification:
2015_09_23-AM-08_05_19
Theory : general
Home
Index