		Search-engine friendly clone of the ACL2 documentation.

Lhatom-var

Lhatom-var->name

Get the name field from a lhatom-var.

Signature
(lhatom-var->name x) → name
Arguments: x — Guard (lhatom-p x).
Returns: name — Type (svar-p name).

This is an ordinary field accessor created by defprod.

Definitions and Theorems

Function: lhatom-var->name$inline

(defun lhatom-var->name$inline (x)
 (declare (xargs :guard (lhatom-p x)))
 (declare (xargs :guard (equal (lhatom-kind x) :var)))
 (let ((__function__ 'lhatom-var->name))
   (declare (ignorable __function__))
   (mbe :logic
        (b* ((x (and (equal (lhatom-kind x) :var) x)))
          (svar-fix (if (or (atom x)
                            (and (eq (car x) :var) (consp (cdr x))))
                        x
                      (car x))))
        :exec
        (if (or (atom x)
                (and (eq (car x) :var) (consp (cdr x))))
            x
          (car x)))))

Theorem: svar-p-of-lhatom-var->name

(defthm svar-p-of-lhatom-var->name
  (b* ((name (lhatom-var->name$inline x)))
    (svar-p name))
  :rule-classes :rewrite)

Theorem: lhatom-var->name$inline-of-lhatom-fix-x

(defthm lhatom-var->name$inline-of-lhatom-fix-x
  (equal (lhatom-var->name$inline (lhatom-fix x))
         (lhatom-var->name$inline x)))

Theorem: lhatom-var->name$inline-lhatom-equiv-congruence-on-x

(defthm lhatom-var->name$inline-lhatom-equiv-congruence-on-x
  (implies (lhatom-equiv x x-equiv)
           (equal (lhatom-var->name$inline x)
                  (lhatom-var->name$inline x-equiv)))
  :rule-classes :congruence)

Theorem: lhatom-var->name-when-wrong-kind

(defthm lhatom-var->name-when-wrong-kind
  (implies (not (equal (lhatom-kind x) :var))
           (equal (lhatom-var->name x)
                  (svar-fix nil))))