Nuprl Definition : record+
T; z:B[self] == self:T ⋂ x:Atom ⟶ if x =a z then B[self] else Top fi
Definitions occuring in Statement :
dep-isect: x:A ⋂ B[x],
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
top: Top,
function: x:A ⟶ B[x],
atom: Atom
Definitions occuring in definition :
dep-isect: x:A ⋂ B[x],
function: x:A ⟶ B[x],
atom: Atom,
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
top: Top
FDL editor aliases :
record+
Latex:
T; z:B[self] == self:T \mcap{} x:Atom {}\mrightarrow{} if x =a z then B[self] else Top fi
Date html generated:
2016_05_15-PM-06_38_43
Last ObjectModification:
2015_09_23-AM-08_04_49
Theory : general
Home
Index