		Search-engine friendly clone of the ACL2 documentation.

Atj-pre-translation-var-reuse

Atj-unmark-var

Decompose a marked variable into its marking and its unmarked name.

Signature
(atj-unmark-var var) → (mv unmarked-var new?)
Arguments: var — Guard (symbolp var).
Returns: unmarked-var — Type (symbolp unmarked-var).; new? — Type (booleanp new?).

The marking is a boolean: t for `new', nil for `old'.

Definitions and Theorems

Function: atj-unmark-var

(defun atj-unmark-var (var)
  (declare (xargs :guard (symbolp var)))
  (let ((__function__ 'atj-unmark-var))
    (declare (ignorable __function__))
    (b* ((string (symbol-name var))
         ((unless (and (>= (length string) 5)
                       (member-equal (subseq string 0 3)
                                     '("[N]" "[O]"))))
          (raise "Internal error: ~x0 has the wrong format."
                 var)
          (mv nil nil))
         (new? (eql (char string 1) #\N))
         (unmarked-string (subseq string 3 (length string)))
         (unmarked-var
              (intern-in-package-of-symbol unmarked-string var)))
      (mv unmarked-var new?))))

Theorem: symbolp-of-atj-unmark-var.unmarked-var

(defthm symbolp-of-atj-unmark-var.unmarked-var
  (b* (((mv ?unmarked-var ?new?)
        (atj-unmark-var var)))
    (symbolp unmarked-var))
  :rule-classes :rewrite)

Theorem: booleanp-of-atj-unmark-var.new?

(defthm booleanp-of-atj-unmark-var.new?
  (b* (((mv ?unmarked-var ?new?)
        (atj-unmark-var var)))
    (booleanp new?))
  :rule-classes :rewrite)