		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Check-expr-iconst

Check if an expression is an integer constant, returning the integer constant if the check passes.

Signature
(check-expr-iconst expr) → iconst?
Arguments: expr — Guard (exprp expr).
Returns: iconst? — Type (iconst-optionp iconst?).

Definitions and Theorems

Function: check-expr-iconst

(defun check-expr-iconst (expr)
  (declare (xargs :guard (exprp expr)))
  (let ((__function__ 'check-expr-iconst))
    (declare (ignorable __function__))
    (b* (((unless (expr-case expr :const)) nil)
         (const (expr-const->const expr))
         ((unless (const-case const :int)))
         (iconst (const-int->unwrap const)))
      iconst)))

Theorem: iconst-optionp-of-check-expr-iconst

(defthm iconst-optionp-of-check-expr-iconst
  (b* ((iconst? (check-expr-iconst expr)))
    (iconst-optionp iconst?))
  :rule-classes :rewrite)

Theorem: check-expr-iconst-of-expr-fix-expr

(defthm check-expr-iconst-of-expr-fix-expr
  (equal (check-expr-iconst (expr-fix expr))
         (check-expr-iconst expr)))

Theorem: check-expr-iconst-expr-equiv-congruence-on-expr

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