		Search-engine friendly clone of the ACL2 documentation.

Atj-pre-translation-type-annotation

Atj-type-unannotate-var

Decompose an annotated ACL2 variable into its unannotated counterpart and its types.

Signature
(atj-type-unannotate-var var) → (mv unannotated-var types)
Arguments: var — Guard (symbolp var).
Returns: unannotated-var — Type (symbolp unannotated-var).; types — Type (atj-type-listp types).

This is the inverse of atj-type-annotate-var.

Definitions and Theorems

Function: atj-type-unannotate-var

(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: symbolp-of-atj-type-unannotate-var.unannotated-var

(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: atj-type-listp-of-atj-type-unannotate-var.types

(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: consp-of-atj-type-unannotate-var.types

(defthm consp-of-atj-type-unannotate-var.types
  (b* (((mv ?unannotated-var ?types)
        (atj-type-unannotate-var var)))
    (consp types))
  :rule-classes :type-prescription)