cons-pos-alistp

(in-package "ACL2")

(defalist cons-pos-alistp
  (x)
  :parents (std/typed-alists)
  :short "Recognize alists from @(tsee cons) pairs to positive integers."
  :key (consp x)
  :val (posp x)
  :true-listp t
  :keyp-of-nil nil
  :valp-of-nil nil
  ///
  (defthm posp-of-cdr-of-assoc-equal-when-cons-pos-alistp
    (implies (cons-pos-alistp alist)
      (iff (posp (cdr (assoc-equal key alist)))
        (assoc-equal key alist)))))