		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-annop

Iconst-annop

Signature
(iconst-annop iconst) → fty::result
Arguments: iconst — Guard (iconstp iconst).
Returns: fty::result — Type (booleanp fty::result).

Definitions and Theorems

Function: iconst-annop

(defun iconst-annop (iconst)
  (declare (xargs :guard (iconstp iconst)))
  (declare (ignorable iconst))
  (let ((__function__ 'iconst-annop))
    (declare (ignorable __function__))
    (iconst-infop (iconst->info iconst))))

Theorem: booleanp-of-iconst-annop

(defthm booleanp-of-iconst-annop
  (b* ((fty::result (iconst-annop iconst)))
    (booleanp fty::result))
  :rule-classes :rewrite)

Theorem: iconst-annop-of-iconst-fix-iconst

(defthm iconst-annop-of-iconst-fix-iconst
  (equal (iconst-annop (iconst-fix iconst))
         (iconst-annop iconst)))

Theorem: iconst-annop-iconst-equiv-congruence-on-iconst

(defthm iconst-annop-iconst-equiv-congruence-on-iconst
  (implies (iconst-equiv iconst iconst-equiv)
           (equal (iconst-annop iconst)
                  (iconst-annop iconst-equiv)))
  :rule-classes :congruence)