		Search-engine friendly clone of the ACL2 documentation.

Alist-map-vals

Values of the map represented by an alist.

General Forms:
(alist-map-vals alist)
(alist-map-vals alist :test 'eql)   ; same as above (eql as equality test)
(alist-map-vals alist :test 'eq)    ; same, but eq is equality test
(alist-map-vals alist :test 'equal) ; same, but equal is equality test

This returns the list of values of the alist, after removing any shadowed pairs. When an alist represents a map, any shadowed pairs are irrelevant. This function is similar to strip-cdrs and alist-vals, except that these two may return values from shadowed pairs. This function is a companion of alist-map-keys. This function returns the range or image (depending on nomenclature) of the map represented by an alist.

The optional keyword, :test, has no effect logically, but provides the test (default eql) used for comparing the keys of the alist in order to remove shadowed pairs.

The guard for a call of alist-map-vals depends on the test. In all cases, the argument must satisfy alistp. If the test is eql, the argument must satisfy eqlable-alistp. If the test is eq, the argument must satisfy symbol-alistp.

See equality-variants for a discussion of the relation between alist-map-vals and its variants:

(alist-map-vals-eq alist) is equivalent to (alist-map-vals alist :test 'eq);
(alist-map-vals-equal alist) is equivalent to (alist-map-vals alist :test 'equal).

In particular, reasoning about any of these primitives reduces to reasoning about the function alist-map-vals-equal.

Subtopics

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