The function
creates definitions with typing lemmas. The term tdef should have structure
where 
and 
.
The term lhs is the new term being defined and the term rhs
is what it is being defined as. All the free variables in lhs should
be appropriately typed in the context 
.
place is a library position.
On evaluation of def, a display form object opid _df, an abstraction opid, and a typing lemma opid_wf are created. The typing lemma is constructed from the tdef term. It has form:
An attempt is made to prove it by unfolding the abstraction and running the Auto tactic. In most cases, this attempt succeeds in completely proving the lemma.
Note that the so_apply abstraction should be used for the second-order variables in the lhs and rhs terms. def takes care of converting these to second-order variables for the abstraction object.
When doing proofs, the basic tactics for folding and unfolding definitions
are the Fold and Unfold tactics. See Chapter 
for
details.
Currently, the only kinds of parameter variables that can be used in typed definitions are level expression variables. This is because Nuprl doesn't currently allow any other kinds of parameter variables in lemma goals and in proofs. Hopefully this should be fixed soon.
An example invocation of def is:
This creates the library objects
