		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Modscope->modidx

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

Definitions and Theorems

Function: modscope->modidx

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

Theorem: natp-of-modscope->modidx

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

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

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

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

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