string-string-alistp

(in-package "ACL2")

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