		Search-engine friendly clone of the ACL2 documentation.

Kestrel-utilities

Make-keyword-value-list-from-keys-and-value

Make a list satisfying keyword-value-listp by associating each member of a true-list of keywords list of keywords with a given value.

Signature
(make-keyword-value-list-from-keys-and-value keys val) → kvlist
Arguments: keys — Guard (keyword-listp keys).
Returns: kvlist — Type (keyword-value-listp kvlist), given the guard.

The keywords in the result are in the same order as in the input keys.

Definitions and Theorems

Function: make-keyword-value-list-from-keys-and-value

(defun make-keyword-value-list-from-keys-and-value (keys val)
 (declare (xargs :guard (keyword-listp keys)))
 (let ((__function__ 'make-keyword-value-list-from-keys-and-value))
  (declare (ignorable __function__))
  (cond
   ((endp keys) nil)
   (t (list* (car keys)
             val
             (make-keyword-value-list-from-keys-and-value (cdr keys)
                                                          val))))))

Theorem: keyword-value-listp-of-make-keyword-value-list-from-keys-and-value

(defthm
 keyword-value-listp-of-make-keyword-value-list-from-keys-and-value
 (implies
  (and (keyword-listp keys))
  (b*
   ((kvlist (make-keyword-value-list-from-keys-and-value keys val)))
   (keyword-value-listp kvlist)))
 :rule-classes :rewrite)