Nuprl Definition : C_DVALUEp_ind

C_DVALUEp_ind(v;
              DVp_Null(x)⇒ Null[x];
              DVp_Int(int)⇒ Int[int];
              DVp_Pointer(ptr)⇒ Pointer[ptr];
              DVp_Array(lower,upper,arr)⇒ rec1.Array[lower; upper; arr; rec1];
              DVp_Struct(lbls,struct)⇒ rec2.Struct[lbls; struct; rec2])  ==
  fix((λC_DVALUEp_ind,v. let lbl,v1 = v 
                         in if lbl="Null" then Null[Ax]
                            if lbl="Int" then Int[v1]
                            if lbl="Pointer" then case v1 of inl(x) => Pointer[inl x] | inr(y) => Pointer[inr Ax ]
                            if lbl="Array"
                              then let lower,v2 = v1 
                                   in let upper,v3 = v2 
                                      in Array[lower; upper; v3; λu.(C_DVALUEp_ind (v3 u))]
                            if lbl="Struct" then let lbls,v2 = v1 in Struct[lbls; v2; λu.(C_DVALUEp_ind (v2 u))]
                            else ⊥
                            fi )) 
  v


Definitions occuring in Statement :  bottom: ⊥,  atom_eq: if a=b then c else d fi ,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  spread: spread def,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  inr: inr x ,  inl: inl x,  token: "$token",  axiom: Ax
FDL editor aliases :  C_DVALUEp_ind
C\_DVALUEp\_ind(v;
                            DVp\_Null(x){}\mRightarrow{}  Null[x];
                            DVp\_Int(int){}\mRightarrow{}  Int[int];
                            DVp\_Pointer(ptr){}\mRightarrow{}  Pointer[ptr];
                            DVp\_Array(lower,upper,arr){}\mRightarrow{}  rec1.Array[lower;  upper;  arr;  rec1];
                            DVp\_Struct(lbls,struct){}\mRightarrow{}  rec2.Struct[lbls;  struct;  rec2])    ==
    fix((\mlambda{}C\_DVALUEp$_{ind}$,v.  let  lbl,v1  =  v 
                                                in  if  lbl="Null"  then  Null[Ax]
                                                      if  lbl="Int"  then  Int[v1]
                                                      if  lbl="Pointer"
                                                          then  case  v1  of  inl(x)  =>  Pointer[inl  x]  |  inr(y)  =>  Pointer[inr  Ax  ]
                                                      if  lbl="Array"
                                                          then  let  lower,v2  =  v1 
                                                                    in  let  upper,v3  =  v2 
                                                                          in  Array[lower;  upper;  v3;  \mlambda{}u.(C\_DVALUEp$_{ind}\000C$  (v3  u))]
                                                      if  lbl="Struct"
                                                          then  let  lbls,v2  =  v1 
                                                                    in  Struct[lbls;  v2;  \mlambda{}u.(C\_DVALUEp$_{ind}$  (v2  \000Cu))]
                                                      else  \mbot{}
                                                      fi  )) 
    v


Date html generated: 2015_07_17-AM-07_45_01
Last ObjectModification: 2014_06_08-PM-03_28_25

Home Index