Nuprl Definition : C_DVALUEp_ind

              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 
                         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 )) 

Definitions occuring in Statement :  bottom: atom_eq: if a=b then else fi  apply: a fix: fix(F) lambda: λx.A[x] spread: spread def decide: case of inl(x) => s[x] inr(y) => t[y] inr: inr  inl: inl x token: "$token" axiom: Ax
FDL editor aliases :  C_DVALUEp_ind
                            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  )) 

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

Home Index