Nuprl Definition : C_TYPEco
C_TYPEco() ==
corec(X.lbl:Atom × if lbl =a "Void" then Unit
if lbl =a "Int" then Unit
if lbl =a "Struct" then (Atom × X) List
if lbl =a "Array" then length:ℕ × X
if lbl =a "Pointer" then X
else Void
fi )
Definitions occuring in Statement :
list: T List,
corec: corec(T.F[T]),
nat: ℕ,
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
unit: Unit,
product: x:A × B[x],
token: "$token",
atom: Atom,
void: Void
FDL editor aliases :
C_TYPEco
C\_TYPEco() ==
corec(X.lbl:Atom \mtimes{} if lbl =a "Void" then Unit
if lbl =a "Int" then Unit
if lbl =a "Struct" then (Atom \mtimes{} X) List
if lbl =a "Array" then length:\mBbbN{} \mtimes{} X
if lbl =a "Pointer" then X
else Void
fi )
Date html generated:
2015_07_17-AM-07_41_59
Last ObjectModification:
2014_06_02-PM-05_22_21
Home
Index