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