Nuprl Rule : mlComputation

H  ⊢ t = tt

  BY mlComputation ()
     
     CallLisp(ML-COMPUTATION)
  No Subgoals


Definitions occuring in rule :  equal: s = t ∈ T,  bool: 𝔹,  btrue: tt,  axiom: Ax
Latex:
H    \mvdash{}  t  =  tt

    BY  mlComputation  ()
         
          CallLisp(ML-COMPUTATION)
    No  Subgoals


Date html generated: 2019_06_20-PM-04_12_02
Last ObjectModification: 2017_05_12-PM-01_51_23

Theory : rules


Home Index