The primitive refinement rules are all introduced by rule objects . The current system has primitive rules for a constructive type-theory, with Martin-Löf predicative semantics. All proofs in the Nuprl system are eventually justified by these primitive rules. More precisely, the correctness of every Nuprl proof depends only on the correctness of these rules, and of Nuprl's refiner . The refiner is a fixed piece of Lisp code which applies primitive rules to unrefined leaves of proofs. Users rarely invoke primitive rules directly; they are at too low a level, and one has to understand how logic is coded within type-theory. Almost always, tactics are used instead.