		Search-engine friendly clone of the ACL2 documentation.

Std/system

Known-packages+

Enhanced variant of known-packages.

Signature
(known-packages+ state) → pkg-names
Returns: pkg-names — Type (string-listp pkg-names).

This returns the same result as known-packages, but it 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 state.

Definitions and Theorems

Function: known-packages+

(defun known-packages+ (state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard t))
 (let ((__function__ 'known-packages+))
  (declare (ignorable __function__))
  (b* ((result (known-packages state)))
   (if (string-listp result)
       result
    (raise
     "Internal error: ~
              the list of keys ~x0 of the alist of known packages ~
              is not a true list of strings."
     result)))))

Theorem: string-listp-of-known-packages+

(defthm string-listp-of-known-packages+
  (b* ((pkg-names (known-packages+ state)))
    (string-listp pkg-names))
  :rule-classes :rewrite)