		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)))))