		Search-engine friendly clone of the ACL2 documentation.

Init-declor-info

Init-declor-info->uid?

Get the uid? field from a init-declor-info.

Signature
(init-declor-info->uid? x) → uid?
Arguments: x — Guard (init-declor-infop x).
Returns: uid? — Type (uid-optionp uid?).

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

Definitions and Theorems

Function: init-declor-info->uid?$inline

(defun init-declor-info->uid?$inline (x)
  (declare (xargs :guard (init-declor-infop x)))
  (declare (xargs :guard t))
  (mbe :logic
       (b* ((x (and t x)))
         (uid-option-fix (cdr (std::da-nth 2 x))))
       :exec (cdr (std::da-nth 2 x))))

Theorem: uid-optionp-of-init-declor-info->uid?

(defthm uid-optionp-of-init-declor-info->uid?
  (b* ((uid? (init-declor-info->uid?$inline x)))
    (uid-optionp uid?))
  :rule-classes :rewrite)

Theorem: init-declor-info->uid?$inline-of-init-declor-info-fix-x

(defthm init-declor-info->uid?$inline-of-init-declor-info-fix-x
  (equal (init-declor-info->uid?$inline (init-declor-info-fix x))
         (init-declor-info->uid?$inline x)))

Theorem: init-declor-info->uid?$inline-init-declor-info-equiv-congruence-on-x

(defthm
 init-declor-info->uid?$inline-init-declor-info-equiv-congruence-on-x
 (implies (init-declor-info-equiv x x-equiv)
          (equal (init-declor-info->uid?$inline x)
                 (init-declor-info->uid?$inline x-equiv)))
 :rule-classes :congruence)