Induction machine of a named logic-mode (singly) recursive function.
(induction-machine fn wrld) → result
- fn — Guard (symbolp fn).
- wrld — Guard (plist-worldp wrld).
- 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
induction is not directly supported for mutually recursive functions.
See induction-machine+ for
an enhanced variant of this utility.
Definitions and Theorems
(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