		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Expression-sub

Abbreviation to construct a subtraction.

Signature
(expression-sub expr1 expr2) → sub-expr
Arguments: expr1 — Guard (expressionp expr1).; expr2 — Guard (expressionp expr2).
Returns: sub-expr — Type (expressionp sub-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-sub

(defun expression-sub (expr1 expr2)
  (declare (xargs :guard (and (expressionp expr1)
                              (expressionp expr2))))
  (let ((__function__ 'expression-sub))
    (declare (ignorable __function__))
    (expression-add expr1 (expression-neg expr2))))

Theorem: expressionp-of-expression-sub

(defthm expressionp-of-expression-sub
  (b* ((sub-expr (expression-sub expr1 expr2)))
    (expressionp sub-expr))
  :rule-classes :rewrite)