Nuprl Rule : direct_computation

H  ⊢ ext t

  BY direct_computation S
     
     Let CallLisp(DIRECT-COMPUTATION)
  H  ⊢ ext t


Latex:
H    \mvdash{}  T  ext  t

    BY  direct\_computation  S
         
          Let  C  =  CallLisp(DIRECT-COMPUTATION)
    H    \mvdash{}  C  ext  t



Date html generated: 2019_06_20-PM-04_12_12
Last ObjectModification: 2016_01_08-PM-11_05_05

Theory : rules


Home Index