Decompose an annotated ACL2 variable into its unannotated counterpart and its types.
(atj-type-unannotate-var var) → (mv unannotated-var types)
This is the inverse of atj-type-annotate-var.
Function:
(defun atj-type-unannotate-var (var) (declare (xargs :guard (symbolp var))) (let ((__function__ 'atj-type-unannotate-var)) (declare (ignorable __function__)) (b* ((string (symbol-name var)) ((unless (and (> (length string) 0) (eql (char string 0) #\[))) (raise "Internal error: ~x0 is not an annotated variable." var) (mv nil (list (atj-type-irrelevant)))) (pos (position #\] string)) ((unless (natp pos)) (raise "Internal error: ~x0 is not an annotated variable." var) (mv nil (list (atj-type-irrelevant)))) (types-id (subseq string 1 pos)) (types (atj-types-of-id types-id)) (unannotated-string (subseq string (1+ pos) (length string))) (unannotated-var (intern-in-package-of-symbol unannotated-string var))) (mv unannotated-var types))))
Theorem:
(defthm symbolp-of-atj-type-unannotate-var.unannotated-var (b* (((mv ?unannotated-var ?types) (atj-type-unannotate-var var))) (symbolp unannotated-var)) :rule-classes :rewrite)
Theorem:
(defthm atj-type-listp-of-atj-type-unannotate-var.types (b* (((mv ?unannotated-var ?types) (atj-type-unannotate-var var))) (atj-type-listp types)) :rule-classes :rewrite)
Theorem:
(defthm consp-of-atj-type-unannotate-var.types (b* (((mv ?unannotated-var ?types) (atj-type-unannotate-var var))) (consp types)) :rule-classes :type-prescription)