		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Expression-neg

Abbreviation to construct a negation.

Signature
(expression-neg expr) → neg-expr
Arguments: expr — Guard (expressionp expr).
Returns: neg-expr — Type (expressionp neg-expr).

This may be added to the abstract syntax at some point. For now it is just an ephemeral abbreviation.

Definitions and Theorems

Function: expression-neg

(defun expression-neg (expr)
  (declare (xargs :guard (expressionp expr)))
  (let ((__function__ 'expression-neg))
    (declare (ignorable __function__))
    (expression-mul (expression-const -1)
                    expr)))

Theorem: expressionp-of-expression-neg

(defthm expressionp-of-expression-neg
  (b* ((neg-expr (expression-neg expr)))
    (expressionp neg-expr))
  :rule-classes :rewrite)