		Search-engine friendly clone of the ACL2 documentation.

Var-sinfo

Var-sinfo->defstatus

Get the defstatus field from a var-sinfo.

Signature
(var-sinfo->defstatus x) → defstatus
Arguments: x — Guard (var-sinfop x).
Returns: defstatus — Type (var-defstatusp defstatus).

This is an ordinary field accessor created by fty::defprod.

Definitions and Theorems

Function: var-sinfo->defstatus$inline

(defun var-sinfo->defstatus$inline (x)
  (declare (xargs :guard (var-sinfop x)))
  (declare (xargs :guard t))
  (let ((__function__ 'var-sinfo->defstatus))
    (declare (ignorable __function__))
    (mbe :logic
         (b* ((x (and t x)))
           (var-defstatus-fix (cdr (std::da-nth 1 x))))
         :exec (cdr (std::da-nth 1 x)))))

Theorem: var-defstatusp-of-var-sinfo->defstatus

(defthm var-defstatusp-of-var-sinfo->defstatus
  (b* ((defstatus (var-sinfo->defstatus$inline x)))
    (var-defstatusp defstatus))
  :rule-classes :rewrite)

Theorem: var-sinfo->defstatus$inline-of-var-sinfo-fix-x

(defthm var-sinfo->defstatus$inline-of-var-sinfo-fix-x
  (equal (var-sinfo->defstatus$inline (var-sinfo-fix x))
         (var-sinfo->defstatus$inline x)))

Theorem: var-sinfo->defstatus$inline-var-sinfo-equiv-congruence-on-x

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