symbol-string-alistp

(in-package "ACL2")

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