		Search-engine friendly clone of the ACL2 documentation.

Dynamic-semantics

Exec-const

Execute a constant.

Signature
(exec-const c) → eval
Arguments: c — Guard (constp c).
Returns: eval — Type (expr-value-resultp eval).

This is just a wrapper of eval-const that returns an expression value (with no object designator), to formalize the execution of the constant as an expression.

Definitions and Theorems

Function: exec-const

(defun exec-const (c)
  (declare (xargs :guard (constp c)))
  (let ((__function__ 'exec-const))
    (declare (ignorable __function__))
    (b* ((val (eval-const c))
         ((when (errorp val)) val))
      (make-expr-value :value val
                       :object nil))))

Theorem: expr-value-resultp-of-exec-const

(defthm expr-value-resultp-of-exec-const
  (b* ((eval (exec-const c)))
    (expr-value-resultp eval))
  :rule-classes :rewrite)

Theorem: exec-const-of-const-fix-c

(defthm exec-const-of-const-fix-c
  (equal (exec-const (const-fix c))
         (exec-const c)))

Theorem: exec-const-const-equiv-congruence-on-c

(defthm exec-const-const-equiv-congruence-on-c
  (implies (const-equiv c c-equiv)
           (equal (exec-const c)
                  (exec-const c-equiv)))
  :rule-classes :congruence)