		Search-engine friendly clone of the ACL2 documentation.

Formalized-subset

Expr-call-formalp

Check if an expression has formal dynamic semantics, as a call expression.

Signature
(expr-call-formalp expr) → yes/no
Arguments: expr — Guard (exprp expr).
Returns: yes/no — Type (booleanp yes/no).

These are the expressions supported by c::exec-expr-call. The expression must be a function call, the function sub-expression must be an identifier, and the arguments must be supported pure expressions.

Definitions and Theorems

Function: expr-call-formalp

(defun expr-call-formalp (expr)
 (declare (xargs :guard (exprp expr)))
 (declare (xargs :guard (expr-unambp expr)))
 (let ((__function__ 'expr-call-formalp))
   (declare (ignorable __function__))
   (and (expr-case expr :funcall)
        (expr-case (expr-funcall->fun expr)
                   :ident)
        (ident-formalp (expr-ident->ident (expr-funcall->fun expr)))
        (expr-list-pure-formalp (expr-funcall->args expr)))))

Theorem: booleanp-of-expr-call-formalp

(defthm booleanp-of-expr-call-formalp
  (b* ((yes/no (expr-call-formalp expr)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: expr-call-formalp-of-expr-fix-expr

(defthm expr-call-formalp-of-expr-fix-expr
  (equal (expr-call-formalp (expr-fix expr))
         (expr-call-formalp expr)))

Theorem: expr-call-formalp-expr-equiv-congruence-on-expr

(defthm expr-call-formalp-expr-equiv-congruence-on-expr
  (implies (expr-equiv expr expr-equiv)
           (equal (expr-call-formalp expr)
                  (expr-call-formalp expr-equiv)))
  :rule-classes :congruence)