Fully partition a wire name.
(typo-partition x) → parts
Function:
(defun typo-partition (x) (declare (xargs :guard (character-listp x))) (let ((__function__ 'typo-partition)) (declare (ignorable __function__)) (b* (((when (atom x)) nil) ((mv prefix remainder) (typo-read-part x)) ((unless prefix) nil)) (cons prefix (typo-partition remainder)))))
Theorem:
(defthm character-list-listp-of-typo-partition (implies (and (force (character-listp x))) (b* ((parts (typo-partition x))) (character-list-listp parts))) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-typo-partition (true-listp (typo-partition x)) :rule-classes :type-prescription)