		Search-engine friendly clone of the ACL2 documentation.

Syndef::acid4

Syndef::acid4->id

Get the syndef::id field from a syndef::acid4.

Signature
(syndef::|acid4->id| syndef::x) → syndef::|id|
Arguments: syndef::x — Guard (syndef::|acid4-P| syndef::x).
Returns: syndef::|id| — Type (integerp syndef::|id|).

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

Definitions and Theorems

Function: acid4->id$inline

(defun syndef::|acid4->id$INLINE| (syndef::x)
  (declare (xargs :guard (syndef::|acid4-P| syndef::x)))
  (declare (xargs :guard t))
  (let ((__function__ 'syndef::|acid4->id|))
    (declare (ignorable __function__))
    (mbe :logic
         (b* ((syndef::x (and t syndef::x)))
           (ifix (cdr (std::da-nth 0 (cdr syndef::x)))))
         :exec (cdr (std::da-nth 0 (cdr syndef::x))))))

Theorem: integerp-of-acid4->id

(defthm syndef::|INTEGERP-OF-acid4->id|
  (b* ((syndef::|id| (syndef::|acid4->id$INLINE| syndef::x)))
    (integerp syndef::|id|))
  :rule-classes :rewrite)

Theorem: acid4->id$inline-of-acid4-fix-x

(defthm syndef::|acid4->id$INLINE-OF-acid4-FIX-X|
 (equal (syndef::|acid4->id$INLINE| (syndef::|acid4-FIX| syndef::x))
        (syndef::|acid4->id$INLINE| syndef::x)))

Theorem: acid4->id$inline-acid4-equiv-congruence-on-x

(defthm syndef::|acid4->id$INLINE-acid4-EQUIV-CONGRUENCE-ON-X|
  (implies (syndef::|acid4-EQUIV| syndef::x syndef::x-equiv)
           (equal (syndef::|acid4->id$INLINE| syndef::x)
                  (syndef::|acid4->id$INLINE| syndef::x-equiv)))
  :rule-classes :congruence)