Nuprl Rule : cutEval

H J ⊢ T ext eval x = s in t

  BY cutEval #$i S x

  H J ⊢ S ext s
  H J ⊢ value-type(S)
  H x:S, J ⊢ T 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: 2019_06_20-PM-04_12_02 Last ObjectModification: 2015_11_25-PM-03_46_57 Theory : rules Home Index