		Search-engine friendly clone of the ACL2 documentation.

Arithmetic-operations

Op-neg

Leo negation operation.

Signature
(op-neg arg curve) → result
Arguments: arg — Guard (valuep arg).; curve — Guard (curvep curve).
Returns: result — Type (value-resultp result).

Definitions and Theorems

Function: op-neg

(defun op-neg (arg curve)
  (declare (xargs :guard (and (valuep arg) (curvep curve))))
  (let ((__function__ 'op-neg))
    (declare (ignorable __function__))
    (cond ((int-valuep arg) (op-int-neg arg))
          ((value-case arg :field)
           (op-field-neg arg curve))
          ((value-case arg :group)
           (op-group-neg arg curve))
          (t (reserrf (list :op-neg (value-fix arg)))))))

Theorem: value-resultp-of-op-neg

(defthm value-resultp-of-op-neg
  (b* ((result (op-neg arg curve)))
    (value-resultp result))
  :rule-classes :rewrite)