Non-empty list of ATJ types identified by a concatenation of short strings.
(atj-types-of-id id) → types
This is the inverse of atj-types-id.
Function:
(defun atj-types-of-id-aux (chars id) (declare (xargs :guard (and (character-listp chars) (stringp id)))) (let ((__function__ 'atj-types-of-id-aux)) (declare (ignorable __function__)) (b* (((when (endp chars)) nil) ((unless (>= (len chars) 2)) (raise "Internal error: ~x0 does not identify a list of types." id)) (first-id (implode (list (first chars) (second chars)))) (first-type (atj-type-of-id first-id)) (rest-types (atj-types-of-id-aux (cddr chars) id))) (cons first-type rest-types))))
Theorem:
(defthm atj-type-listp-of-atj-types-of-id-aux (b* ((types (atj-types-of-id-aux chars id))) (atj-type-listp types)) :rule-classes :rewrite)
Function:
(defun atj-types-of-id (id) (declare (xargs :guard (stringp id))) (let ((__function__ 'atj-types-of-id)) (declare (ignorable __function__)) (b* ((types (atj-types-of-id-aux (explode id) id))) (if (consp types) types (prog2$ (raise "Internal error: ~x0 identifies an empty list of types." id) (list (atj-type-irrelevant)))))))
Theorem:
(defthm atj-type-listp-of-atj-types-of-id (b* ((types (atj-types-of-id id))) (atj-type-listp types)) :rule-classes :rewrite)
Theorem:
(defthm consp-of-atj-types-of-id (b* ((types (atj-types-of-id id))) (consp types)) :rule-classes :type-prescription)