		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Modscope->wireoffset

Signature
(modscope->wireoffset x) → wireoffset
Arguments: x — Guard (modscope-p x).
Returns: wireoffset — Type (natp wireoffset).

Definitions and Theorems

Function: modscope->wireoffset

(defun modscope->wireoffset (x)
  (declare (xargs :guard (modscope-p x)))
  (let ((__function__ 'modscope->wireoffset))
    (declare (ignorable __function__))
    (modscope-case x
                   :top 0
                   :nested x.wireoffset)))

Theorem: natp-of-modscope->wireoffset

(defthm natp-of-modscope->wireoffset
  (b* ((wireoffset (modscope->wireoffset x)))
    (natp wireoffset))
  :rule-classes :type-prescription)

Theorem: modscope->wireoffset-of-modscope-fix-x

(defthm modscope->wireoffset-of-modscope-fix-x
  (equal (modscope->wireoffset (modscope-fix x))
         (modscope->wireoffset x)))

Theorem: modscope->wireoffset-modscope-equiv-congruence-on-x

(defthm modscope->wireoffset-modscope-equiv-congruence-on-x
  (implies (modscope-equiv x x-equiv)
           (equal (modscope->wireoffset x)
                  (modscope->wireoffset x-equiv)))
  :rule-classes :congruence)