		Search-engine friendly clone of the ACL2 documentation.

Std/system/function-queries

Ruler-extenders+

Enhanced variant of ruler-extenders.

Signature
(ruler-extenders+ fn wrld) → ruler-extenders
Arguments: fn — Guard (symbolp fn).; wrld — Guard (plist-worldp wrld).
Returns: ruler-extenders — Type (or (symbol-listp ruler-extenders) (equal ruler-extenders :all)).

This returns the same result as ruler-extenders, but it is guard-verified and includes a run-time check (which should always succeed) on the result that allows us to prove the return type theorem without strengthening the guard on wrld. This utility also includes a run-time check (which should always succeed) on the form of the justification property of the function that allows us to verify the guards without strengthening the guard of wrld. Furthermore, this utility causes an error if called on a symbol that does not name a recursive logic-mode function; the reason for ensuring logic-mode is that recursive program-mode functions do not have ruler extenders.

Definitions and Theorems

Function: ruler-extenders+

(defun
 ruler-extenders+ (fn wrld)
 (declare (xargs :guard (and (symbolp fn) (plist-worldp wrld))))
 (let
  ((__function__ 'ruler-extenders+))
  (declare (ignorable __function__))
  (if
   (not (irecursivep+ fn wrld))
   (raise "The function ~x0 is not recursive." fn)
   (b*
    ((justification (getpropc fn 'justification nil wrld))
     ((unless (weak-justification-p justification))
      (raise
       "Internal error: ~
                  the 'JUSTIFICATION property ~x0 of ~x1 is not well-formed."
       justification fn))
     (ruler-extenders (access justification
                              justification :ruler-extenders))
     ((unless (or (symbol-listp ruler-extenders)
                  (eq ruler-extenders :all)))
      (raise
       "Internal error: ~
                  the well-founded relation ~x0 of ~x1 ~
                  is neither a true list of symbols nor :ALL."
       ruler-extenders fn)))
    ruler-extenders))))

Theorem: return-type-of-ruler-extenders+

(defthm return-type-of-ruler-extenders+
        (b* ((ruler-extenders (ruler-extenders+ fn wrld)))
            (or (symbol-listp ruler-extenders)
                (equal ruler-extenders :all)))
        :rule-classes :rewrite)