		Search-engine friendly clone of the ACL2 documentation.

Error-checking

Ensure-function-not-in-termination-thm

Cause an error if a recursive function occurs in its own termination theorem.

Signature
(ensure-function-not-in-termination-thm fn description error-erp error-val ctx state) → (mv erp val state)
Arguments: fn — Function to check.
Guard (and (logic-function-namep fn (w state)) (recursivep fn nil (w state))) .; description — Guard (msgp description).; error-erp — Flag to return in case of error.; error-val — Value to return in case of error.; ctx — Context for errors.
Returns: erp — nil or error-erp.; val — nil if erp is nil, otherwise error-val.

Definitions and Theorems

Function: ensure-function-not-in-termination-thm

(defun ensure-function-not-in-termination-thm
       (fn description
           error-erp error-val ctx state)
 (declare (xargs :stobjs (state)))
 (declare
      (xargs :guard (and (msgp description)
                         (and (logic-function-namep fn (w state))
                              (recursivep fn nil (w state))))))
 (b*
  (((when
        (member-eq fn
                   (all-ffn-symbs (termination-theorem fn (w state))
                                  nil)))
    (er-soft+
     ctx error-erp error-val
     "~@0 must not occur in its own termination theorem, which is~%~x1."
     description
     (termination-theorem fn (w state)))))
  (value nil)))

Subtopics

Ensure-function-not-in-termination-thm$: Calls ensure-function-not-in-termination-thm with ctx and state as the last two arguments.