symbol-nat-alistp

(in-package "ACL2")

(defalist symbol-nat-alistp
  (x)
  :parents (std/typed-alists)
  :short "Recognize alists from symbols to natural numbers."
  :key (symbolp x)
  :val (natp x)
  :true-listp t
  :keyp-of-nil t
  :valp-of-nil nil
  ///
  (defthm natp-of-cdr-of-assoc-equal-when-symbol-nat-alistp
    (implies (symbol-nat-alistp alist)
      (iff (natp (cdr (assoc-equal key alist)))
        (assoc-equal key alist)))))