		Search-engine friendly clone of the ACL2 documentation.

Constant-propagation

Const-prop-eval-unop-expr

Propogate a constant through a c$::unop.

Signature
(const-prop-eval-unop-expr unop arg) → value?
Arguments: unop — Guard (unopp unop).; arg — Guard (c::valuep arg).
Returns: value? — Type (c::value-optionp value?).

Definitions and Theorems

Function: const-prop-eval-unop-expr

(defun const-prop-eval-unop-expr (unop arg)
 (declare (xargs :guard (and (unopp unop) (c::valuep arg))))
 (let ((__function__ 'const-prop-eval-unop-expr))
  (declare (ignorable __function__))
  (unop-case
   unop
   :plus (value-result-to-option (c::eval-unary (c::unop-plus) arg))
   :minus
   (value-result-to-option (c::eval-unary (c::unop-minus) arg))
   :bitnot
   (value-result-to-option (c::eval-unary (c::unop-bitnot) arg))
   :lognot
   (value-result-to-option (c::eval-unary (c::unop-lognot) arg))
   :otherwise nil)))

Theorem: value-optionp-of-const-prop-eval-unop-expr

(defthm value-optionp-of-const-prop-eval-unop-expr
  (b* ((value? (const-prop-eval-unop-expr unop arg)))
    (c::value-optionp value?))
  :rule-classes :rewrite)