		Search-engine friendly clone of the ACL2 documentation.

Statements

Asgop-to-binop

Map each Leo compound assignment operator to the corresponding binary operator.

Signature
(asgop-to-binop op) → bop
Arguments: op — Guard (asgopp op).
Returns: bop — Type (binopp bop).

Definitions and Theorems

Function: asgop-to-binop

(defun asgop-to-binop (op)
  (declare (xargs :guard (asgopp op)))
  (declare (xargs :guard (not (asgop-case op :asg))))
  (let ((__function__ 'asgop-to-binop))
    (declare (ignorable __function__))
    (asgop-case op
                :asg (prog2$ (impossible)
                             (ec-call (binop-fix :irrelevant)))
                :asg-add (binop-add)
                :asg-sub (binop-sub)
                :asg-mul (binop-mul)
                :asg-div (binop-div)
                :asg-rem (binop-rem)
                :asg-pow (binop-pow)
                :asg-shl (binop-shl)
                :asg-shr (binop-shr)
                :asg-bitand (binop-bitand)
                :asg-bitior (binop-bitior)
                :asg-bitxor (binop-bitxor)
                :asg-and (binop-and)
                :asg-or (binop-or))))

Theorem: binopp-of-asgop-to-binop

(defthm binopp-of-asgop-to-binop
  (b* ((bop (asgop-to-binop op)))
    (binopp bop))
  :rule-classes :rewrite)

Theorem: asgop-to-binop-of-asgop-fix-op

(defthm asgop-to-binop-of-asgop-fix-op
  (equal (asgop-to-binop (asgop-fix op))
         (asgop-to-binop op)))

Theorem: asgop-to-binop-asgop-equiv-congruence-on-op

(defthm asgop-to-binop-asgop-equiv-congruence-on-op
  (implies (asgop-equiv op op-equiv)
           (equal (asgop-to-binop op)
                  (asgop-to-binop op-equiv)))
  :rule-classes :congruence)