		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Check-expr-ident

Check if an expression is an identifier, returning the identifier if the check passes.

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

Definitions and Theorems

Function: check-expr-ident

(defun check-expr-ident (expr)
  (declare (xargs :guard (exprp expr)))
  (let ((__function__ 'check-expr-ident))
    (declare (ignorable __function__))
    (and (expr-case expr :ident)
         (expr-ident->ident expr))))

Theorem: ident-optionp-of-check-expr-ident

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

Theorem: check-expr-ident-of-expr-fix-expr

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

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

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