		Search-engine friendly clone of the ACL2 documentation.

Std/system

Std/system/partition-rest-and-keyword-args

Theorems about partition-rest-and-keyword-args.

Definitions and Theorems

Theorem: true-listp-of-partition-rest-and-keyword.rest

(defthm true-listp-of-partition-rest-and-keyword.rest
  (implies (true-listp x)
           (mv-let (erp rest keypart)
                   (partition-rest-and-keyword-args x keys)
             (declare (ignore keypart))
             (implies (not erp) (true-listp rest))))
  :rule-classes (:rewrite :type-prescription))

Theorem: symbol-alistp-of-partition-rest-and-keyword.keypart

(defthm symbol-alistp-of-partition-rest-and-keyword.keypart
  (implies (true-listp x)
           (mv-let (erp rest keypart)
                   (partition-rest-and-keyword-args x keys)
             (declare (ignore rest))
             (implies (not erp)
                      (symbol-alistp keypart)))))