Nuprl Definition : C_TYPE

Nuprl Definition : C_TYPE_ind

C_TYPE_ind(v
Void=>Void
Int=>Int
Struct(fields)=>rec1.Struct[fields; rec1]
Array(length,elems)=>rec2.Array[length; elems; rec2]
Pointer(to)=>rec3.Pointer[to; rec3]) ==
  fix((λC_TYPE_ind,v. let lbl,v1 = v
                      in if lbl="Void" then Void
                         if lbl="Int" then Int

                         if lbl="Struct" then Struct[v1; λi.let v2,v3 = v1[i] in C_TYPE_ind v3]

                         if lbl="Array" then let length,v2 = v1 in Array[length; v2; C_TYPE_ind v2]

                         if lbl="Pointer" then Pointer[v1; C_TYPE_ind v1]
                         else ⊥
                         fi ))
  v

Definitions occuring in Statement : select: L[n], bottom: ⊥, atom_eq: if a=b then c else d fi , apply: f a, fix: fix(F), lambda: λx.A[x], spread: spread def, token: "$token"
FDL editor aliases : C_TYPE_ind
C\_TYPE\_ind(v Void=>Void Int=>Int Struct(fields)=>rec1.Struct[fields; rec1] Array(length,elems)=>rec2.Array[length; elems; rec2] Pointer(to)=>rec3.Pointer[to; rec3]) == fix((\mlambda{}C\_TYPE$_{ind}$,v. let lbl,v1 = v in if lbl="Void" then Void if lbl="Int" then Int if lbl="Struct" then Struct[v1; \mlambda{}i.let v2,v3 = v1[i] in C\_TYPE$_\mbackslash{}ff7\000Cbind}$ v3] if lbl="Array" then let length,v2 = v1 in Array[length; v2; C\_TYPE$_\000C{ind}$ v2] if lbl="Pointer" then Pointer[v1; C\_TYPE$_{ind}$ v1] else \mbot{} fi )) v Date html generated: 2015_07_17-AM-07_42_31 Last ObjectModification: 2014_06_02-PM-05_27_46 Home Index