		Search-engine friendly clone of the ACL2 documentation.

Std/system/function-queries

Non-executablep+

Enhanced variant of non-executablep.

Signature
(non-executablep+ fn wrld) → nonexec
Arguments: fn — Guard (symbolp fn).; wrld — Guard (plist-worldp wrld).
Returns: nonexec — Type (or (booleanp nonexec) (eq nonexec :program)).

This returns the same result as non-executablep, but it includes run-time checks (which should always succeed) on the result that allow us to prove the return type theorems without strengthening the guard on wrld. Furthermore, this utility causes an error if called on a symbol that does not name a function.

Definitions and Theorems

Function: non-executablep+

(defun non-executablep+ (fn wrld)
 (declare (xargs :guard (and (symbolp fn) (plist-worldp wrld))))
 (let ((__function__ 'non-executablep+))
  (declare (ignorable __function__))
  (if (not (function-symbolp fn wrld))
      (raise "The symbol ~x0 does not name a function."
             fn)
   (b*
    ((result (non-executablep fn wrld))
     ((unless (or (booleanp result)
                  (eq result :program)))
      (raise
       "Internal error: ~
                  the non-executable status ~x0 of ~x1 is not ~
                  T, NIL, or :PROGRAM."
       result fn))
     ((when (and (logicp fn wrld)
                 (eq result :program)))
      (raise
       "Internal error: ~
                  the non-executable status of the logic-mode function ~x0 ~
                  is :PROGRAM instead of T or NIL."
       fn)))
    result))))

Theorem: return-type-of-non-executablep+

(defthm return-type-of-non-executablep+
  (b* ((nonexec (non-executablep+ fn wrld)))
    (or (booleanp nonexec)
        (eq nonexec :program)))
  :rule-classes :rewrite)

Theorem: booleanp-of-non-executablep+-when-logicp

(defthm booleanp-of-non-executablep+-when-logicp
  (implies (logicp fn wrld)
           (b* ((nonexec (non-executablep+ fn wrld)))
             (booleanp nonexec)))
  :rule-classes :rewrite)