induction-machine

(in-package "ACL2")

(define induction-machine
  ((fn symbolp) (wrld plist-worldp))
  :returns (result "A @(tsee pseudo-tests-and-calls-listp).")
  :parents (std/system/function-queries)
  :short "Induction machine of a named logic-mode (singly) recursive function."
  :long (topstring (p "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').")
    (p "Note that
     induction is not directly supported for mutually recursive functions.")
    (p "See @(tsee induction-machine+) for
     an enhanced variant of this utility."))
  (getpropc fn 'induction-machine nil wrld))