Nuprl Definition : C_LVALUE_ind
C_LVALUE_ind(v;
             LV_Ground(loc)
⇒ Ground[loc];
             LV_Index(lval,idx)
⇒ rec1.Index[lval; idx; rec1];
             LV_Scomp(lval,comp)
⇒ rec2.Scomp[lval; comp; rec2])  ==
  fix((λC_LVALUE_ind,v. let lbl,v1 = v 
                        in if lbl="Ground" then Ground[v1]
                           if lbl="Index" then let lval,v2 = v1 in Index[lval; v2; C_LVALUE_ind lval]
                           if lbl="Scomp" then let lval,v2 = v1 in Scomp[lval; v2; C_LVALUE_ind lval]
                           else Ax
                           fi )) 
  v
Definitions occuring in Statement : 
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"
, 
axiom: Ax
Definitions occuring in definition : 
fix: fix(F)
, 
lambda: λx.A[x]
, 
atom_eq: if a=b then c else d fi 
, 
token: "$token"
, 
spread: spread def, 
apply: f a
, 
axiom: Ax
FDL editor aliases : 
C_LVALUE_ind
C_LVALUE_ind
Latex:
C\_LVALUE\_ind(v;
                          LV\_Ground(loc){}\mRightarrow{}  Ground[loc];
                          LV\_Index(lval,idx){}\mRightarrow{}  rec1.Index[lval;  idx;  rec1];
                          LV\_Scomp(lval,comp){}\mRightarrow{}  rec2.Scomp[lval;  comp;  rec2])    ==
    fix((\mlambda{}C\_LVALUE$_{ind}$,v.  let  lbl,v1  =  v 
                                              in  if  lbl="Ground"  then  Ground[v1]
                                                    if  lbl="Index"  then  let  lval,v2  =  v1  in  Index[lval;  v2;  C\_LVALUE$_\000C{ind}$  lval]
                                                    if  lbl="Scomp"  then  let  lval,v2  =  v1  in  Scomp[lval;  v2;  C\_LVALUE$_\000C{ind}$  lval]
                                                    else  Ax
                                                    fi  )) 
    v
Date html generated:
2016_05_16-AM-08_47_42
Last ObjectModification:
2015_12_14-PM-01_40_04
Theory : C-semantics
Home
Index