Measure
Declare a measure for a defun
See xargs for discussion of how to use the :measure
keyword to specify a measure for a definition. A related utility,
get-measure, may be found in the community-books, file
std/system/get-measure.lisp.
Subtopics
- Termination-theorem-example
- How to use a previously-proved measure theorem
- Measure-debug
- Generate markers to indicate sources of measure proof obligations
- Make-termination-theorem
- Create a copy of a function's termination theorem that calls stubs.
- Termination-theorem
- Use a (functional instance of a) previously-proved measure theorem
- Tthm
- The measure (termination) theorem for a given function symbol
