Nuprl Definition : binary_mapco
binary_mapco(T;Key) ==
corec(X.lbl:Atom × if lbl =a "E" then Unit
if lbl =a "T" then key:Key × value:T × cnt:ℤ × left:X × X
else Void
fi )
Definitions occuring in Statement :
corec: corec(T.F[T]),
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
unit: Unit,
product: x:A × B[x],
int: ℤ,
token: "$token",
atom: Atom,
void: Void
FDL editor aliases :
binary_mapco
Latex:
binary\_mapco(T;Key) ==
corec(X.lbl:Atom \mtimes{} if lbl =a "E" then Unit
if lbl =a "T" then key:Key \mtimes{} value:T \mtimes{} cnt:\mBbbZ{} \mtimes{} left:X \mtimes{} X
else Void
fi )
Date html generated:
2016_05_17-PM-01_36_51
Last ObjectModification:
2014_04_30-AM-11_03_56
Theory : binary-map
Home
Index