Objects

There are seven kinds of objects:

rule 

A rule object defines a primitive rule of the object logic.

theorem 

A theorem object contains a proposition and a proof. If the proof is complete, the proposition is a theorem. If incomplete, a conjecture  . A proof maybe   or  . Theorems are sometimes referred to as lemmas  . A theorem object for a complete theorem also contains the extract term  of the theorem.

abstraction 

An abstraction object introduces the definition  of a new term.

ml 

An ml object  contains ML code.

display 

A display object defines display forms  for primitive terms and abstractions.

precedence 

A precedence object assigns precedences for terms. Precedences control the automatic parenthesization of terms.

comment 

A comment object contains a comment. Comments have no logical significance.

Theorem objects are discussed more in Chapter and the rest of the kinds of object are discussed more in Chapter .

Every object has associated with it a status  , either raw , bad , incomplete  or complete , indicating the current state of the object. A raw status means an object has been changed but not yet checked. A bad status means an object has been checked and found to contain errors. An incomplete status is meaningful only for theorem objects and signifies that its proof contains no errors but has not been finished. A complete status indicates that the object is correct and complete.