Nuprl Definition : C_DVALUEpco
C_DVALUEpco() ==
corec(X.lbl:Atom × if lbl =a "Null" then Unit
if lbl =a "Int" then ℤ
if lbl =a "Pointer" then C_LVALUE()?
if lbl =a "Array" then lower:ℤ × upper:ℤ × ({lower..upper-} ─→ X)
if lbl =a "Struct" then lbls:Atom List × ({a:Atom| (a ∈ lbls)} ─→ X)
else Void
fi )
Definitions occuring in Statement :
C_LVALUE: C_LVALUE(),
l_member: (x ∈ l),
list: T List,
corec: corec(T.F[T]),
int_seg: {i..j-},
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
unit: Unit,
set: {x:A| B[x]} ,
function: x:A ─→ B[x],
product: x:A × B[x],
union: left + right,
int: ℤ,
token: "$token",
atom: Atom,
void: Void
FDL editor aliases :
C_DVALUEpco
C\_DVALUEpco() ==
corec(X.lbl:Atom \mtimes{} if lbl =a "Null" then Unit
if lbl =a "Int" then \mBbbZ{}
if lbl =a "Pointer" then C\_LVALUE()?
if lbl =a "Array" then lower:\mBbbZ{} \mtimes{} upper:\mBbbZ{} \mtimes{} (\{lower..upper\msupminus{}\} {}\mrightarrow{} X)
if lbl =a "Struct" then lbls:Atom List \mtimes{} (\{a:Atom| (a \mmember{} lbls)\} {}\mrightarrow{} X)
else Void
fi )
Date html generated:
2015_07_17-AM-07_43_55
Last ObjectModification:
2014_06_08-PM-03_19_40
Home
Index