		Search-engine friendly clone of the ACL2 documentation.

Std/system/function-queries

Measure

Measure expression of a named logic-mode recursive function.

Signature
(measure fn wrld) → measure
Arguments: fn — Guard (symbolp fn).; wrld — Guard (plist-worldp wrld).
Returns: measure — A pseudo-termp.

See xargs for a discussion of the :measure keyword.

See measure+ for an enhanced variant of this utility.

Definitions and Theorems

Function: measure

(defun measure (fn wrld)
  (declare (xargs :guard (and (symbolp fn) (plist-worldp wrld))))
  (let ((__function__ 'measure))
    (declare (ignorable __function__))
    (b* ((justification (getpropc fn 'justification nil wrld)))
      (access justification justification :measure))))

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