		Search-engine friendly clone of the ACL2 documentation.

Ipasir

Ipasir-get$a

Signature
(ipasir-get$a ipasir$a) → val
Arguments: ipasir$a — Guard (ipasir$a-p ipasir$a).
Returns: val — Type (ipasir$a-p val).

Definitions and Theorems

Function: ipasir-get$a

(defun ipasir-get$a (ipasir$a)
  (declare (xargs :guard (ipasir$a-p ipasir$a)))
  (let ((__function__ 'ipasir-get$a))
    (declare (ignorable __function__))
    (ipasir$a-fix ipasir$a)))

Theorem: ipasir$a-p-of-ipasir-get$a

(defthm ipasir$a-p-of-ipasir-get$a
  (b* ((val (ipasir-get$a ipasir$a)))
    (ipasir$a-p val))
  :rule-classes :rewrite)

Theorem: ipasir-get$a-of-ipasir$a-fix-ipasir$a

(defthm ipasir-get$a-of-ipasir$a-fix-ipasir$a
  (equal (ipasir-get$a (ipasir$a-fix ipasir$a))
         (ipasir-get$a ipasir$a)))

Theorem: ipasir-get$a-ipasir$a-equiv-congruence-on-ipasir$a

(defthm ipasir-get$a-ipasir$a-equiv-congruence-on-ipasir$a
  (implies (ipasir$a-equiv ipasir$a ipasir$a-equiv)
           (equal (ipasir-get$a ipasir$a)
                  (ipasir-get$a ipasir$a-equiv)))
  :rule-classes :congruence)