Nuprl Definition : C_STOREp-welltyped

C_STOREp-welltyped(env;store) ==
  ∀loc:C_LOCATION()
    if isl(env loc)
    then ↑(isl(store loc) ∧b (C_TYPE_vs_DVALp(env;outl(env loc)) outl(store loc)))
    else ↑isr(store loc)
    fi 


Definitions occuring in Statement :  C_TYPE_vs_DVALp: C_TYPE_vs_DVALp(env;ctyp),  C_LOCATION: C_LOCATION(),  band: p ∧b q,  outl: outl(x),  assert: ↑b,  ifthenelse: if b then t else f fi ,  isr: isr(x),  isl: isl(x),  all: ∀x:A. B[x],  apply: f a
FDL editor aliases :  C_STOREp-welltyped
Latex:
C\_STOREp-welltyped(env;store)  ==
    \mforall{}loc:C\_LOCATION()
        if  isl(env  loc)
        then  \muparrow{}(isl(store  loc)  \mwedge{}\msubb{}  (C\_TYPE\_vs\_DVALp(env;outl(env  loc))  outl(store  loc)))
        else  \muparrow{}isr(store  loc)
        fi 


Date html generated: 2016_05_16-AM-08_51_25
Last ObjectModification: 2014_06_09-PM-01_14_13

Theory : C-semantics


Home Index