Nuprl Definition : C

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

Latex:
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: 2016_05_16-AM-08_44_16 Last ObjectModification: 2014_06_02-PM-05_22_21 Theory : C-semantics Home Index