		Search-engine friendly clone of the ACL2 documentation.

Count-keys

Count the number of keys in association list

(Count-keys al) returns the number of distinct keys in an association list.

Count-keys has a guard of t. This function is called in the body of function, <h>-count where <h> is a hash-table field of a stobj. See defstobj.

Function: hons-remove-assoc

(defun hons-remove-assoc (k x)
       (declare (xargs :guard t))
       (if (atom x)
           nil
           (if (and (consp (car x))
                    (not (equal k (caar x))))
               (cons (car x)
                     (hons-remove-assoc k (cdr x)))
               (hons-remove-assoc k (cdr x)))))

Function: count-keys

(defun
     count-keys (al)
     (declare (xargs :guard t))
     (if (atom al)
         0
         (if (consp (car al))
             (+ 1
                (count-keys (hons-remove-assoc (caar al) (cdr al))))
             (count-keys (cdr al)))))