next up previous contents index
Next: Functionality Lemmas Up: Rewriting Previous: Applying Conversions

Lemma Support

   

The rewrite package must have access to several kinds of lemmas in order to construct justifications for rewrites. This section describes those lemmas.

Note that for order relations, one only needs lemmas for one direction. For example, one doesn't require both the lemma

and

If Nuprl finds a lemma missing in the course of constructing a rewrite justification it prints out an error message suggesting the kind and structure of the missing lemma. After entering it, you need to evaluate the function

initialize_rw_lemma_caches : unit -> unit 

on argument () in the ML Top Loop ; for efficiency reasons, the rewrite code caches information about these lemmas and hasn't been set up yet to automatically update caches after changes to the available lemmas in the library.





Karla Consroe
Wed Oct 23 13:48:45 EDT 1996