Nuprl Rule : mlComputation

H  ⊢ tt

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



Definitions occuring in rule :  equal: 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