Nuprl Rule : cutEval

J ⊢ ext eval in t

  BY cutEval #$i x
  
  J ⊢ ext s
  J ⊢ value-type(S)
  x:S, J ⊢ ext t



Definitions occuring in rule :  callbyvalue: callbyvalue value-type: value-type(T) axiom: Ax

Latex:
H  J  \mvdash{}  T  ext  eval  x  =  s  in  t

    BY  cutEval  \#\$i  S  x
   
    H  J  \mvdash{}  S  ext  s
    H  J  \mvdash{}  value-type(S)
    H  x:S,  J  \mvdash{}  T  ext  t



Date html generated: 2016_12_14-AM-08_53_42
Last ObjectModification: 2015_11_25-PM-03_46_57

Theory : rules


Home Index