Build an alist mapping strings to their partitionings.
(typo-partitioning-alist x) → al
Function:
(defun typo-partitioning-alist (x) (declare (xargs :guard (string-listp x))) (let ((__function__ 'typo-partitioning-alist)) (declare (ignorable __function__)) (if (atom x) nil (cons (cons (car x) (typo-partition (explode (car x)))) (typo-partitioning-alist (cdr x))))))
Theorem:
(defthm alistp-of-typo-partitioning-alist (b* ((al (typo-partitioning-alist x))) (alistp al)) :rule-classes :rewrite)
Theorem:
(defthm vl-string-keys-p-of-typo-partitioning-alist (implies (force (string-listp x)) (vl-string-keys-p (typo-partitioning-alist x))))
Theorem:
(defthm vl-character-list-values-p-of-typo-partitioning-alist (vl-character-list-list-values-p (typo-partitioning-alist x)))