• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
      • Alist-keys
      • Remove-assocs
      • Alist-vals
      • Alist-map-vals
        • Alist-map-vals-functions-and-macros
        • Alist-map-vals-theorems
      • Alist-map-keys
      • Std/alists/strip-cdrs
      • Hons-rassoc-equal
      • Std/alists/hons-assoc-equal
      • Std/alists/strip-cars
      • Fal-find-any
      • Fal-extract
      • Std/alists/abstract
      • Fal-extract-vals
      • Fal-all-boundp
      • Std/alists/alistp
      • Append-alist-vals
      • Append-alist-keys
      • Alist-equiv
      • Hons-remove-assoc
      • Std/alists/pairlis$
      • Worth-hashing
      • Alists-agree
      • Sub-alistp
      • Alist-fix
      • Std/alists/remove-assoc-equal
      • Std/alists/assoc-equal
    • Obags
    • Std/util
    • Std/strings
    • Std/io
    • Std/osets
    • Std/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Alist-map-vals

Alist-map-vals-functions-and-macros

Definitions of the alist-map-vals functions and macros, and basic theorems about them.

Definitions and Theorems

Function: alist-map-vals-equal

(defun alist-map-vals-equal (alist)
  (declare (xargs :guard (alistp alist)))
  (cond ((endp alist) nil)
        (t (let* ((pair (car alist))
                  (key (car pair))
                  (val (cdr pair)))
             (cons val
                   (alist-map-vals-equal
                        (remove-assoc-equal key (cdr alist))))))))

Function: alist-map-vals-eq-exec$guard-check

(defun alist-map-vals-eq-exec$guard-check (alist)
  (declare (xargs :guard (symbol-alistp alist)))
  (declare (ignore alist))
  t)

Function: alist-map-vals-eq-exec

(defun alist-map-vals-eq-exec (alist)
 (declare (xargs :guard (symbol-alistp alist)))
 (cond
  ((endp alist) nil)
  (t
   (let* ((pair (car alist))
          (key (car pair))
          (val (cdr pair)))
    (cons
     val
     (alist-map-vals-eq-exec (remove-assoc-eq key (cdr alist))))))))

Function: alist-map-vals-eql-exec$guard-check

(defun alist-map-vals-eql-exec$guard-check (alist)
  (declare (xargs :guard (eqlable-alistp alist)))
  (declare (ignore alist))
  t)

Function: alist-map-vals-eql-exec

(defun alist-map-vals-eql-exec (alist)
 (declare (xargs :guard (eqlable-alistp alist)))
 (cond ((endp alist) nil)
       (t (let* ((pair (car alist))
                 (key (car pair))
                 (val (cdr pair)))
            (cons val
                  (alist-map-vals-eql-exec
                       (remove-assoc-eql-exec key (cdr alist))))))))

Theorem: alist-map-vals-eq-exec-is-alist-map-vals-equal

(defthm alist-map-vals-eq-exec-is-alist-map-vals-equal
  (equal (alist-map-vals-eq-exec alist)
         (alist-map-vals-equal alist)))

Theorem: alist-map-vals-eql-exec-is-alist-map-vals-equal

(defthm alist-map-vals-eql-exec-is-alist-map-vals-equal
  (equal (alist-map-vals-eql-exec alist)
         (alist-map-vals-equal alist)))