		Search-engine friendly clone of the ACL2 documentation.

Std/system/function-queries

Induction-machine

Induction machine of a named logic-mode (singly) recursive function.

Signature
(induction-machine fn wrld) → result
Arguments: fn — Guard (symbolp fn).; wrld — Guard (plist-worldp wrld).
Returns: result — A pseudo-tests-and-calls-listp.

This is a list of tests-and-calls records (see the ACL2 source code for information on these records), each of which contains zero or more recursive calls along with the tests that lead to them. The induction machine is a value of type pseudo-tests-and-calls-listp, which is defined in system/pseudo-tests-and-calls-listp.lisp.

Note that induction is not directly supported for mutually recursive functions.

See induction-machine+ for an enhanced variant of this utility.

Definitions and Theorems

Function: induction-machine

(defun induction-machine (fn wrld)
  (declare (xargs :guard (and (symbolp fn) (plist-worldp wrld))))
  (let ((__function__ 'induction-machine))
    (declare (ignorable __function__))
    (getpropc fn 'induction-machine
              nil wrld)))