		Search-engine friendly clone of the ACL2 documentation.

Constant-propagation

Expr-to-ident

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

Definitions and Theorems

Function: expr-to-ident

(defun expr-to-ident (expr)
  (declare (xargs :guard (exprp expr)))
  (let ((__function__ 'expr-to-ident))
    (declare (ignorable __function__))
    (expr-case expr
               :ident expr.ident
               :otherwise nil)))

Theorem: ident-optionp-of-expr-to-ident

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