Filtering...

negative-syntaxp

books/rtl/rel9/arithmetic/negative-syntaxp
other
(in-package "ACL2")
negative-syntaxpfunction
(defun negative-syntaxp
  (term)
  (if (not (consp term))
    nil
    (case (car term)
      '(and (rationalp (cadr term)) (< (cadr term) 0))
      (unary-- (not (negative-syntaxp (cadr term))))
      (binary-+ (and (negative-syntaxp (cadr term))
          (negative-syntaxp (caddr term))))
      (binary-* (and (or (and (negative-syntaxp (cadr term))
              (not (negative-syntaxp (caddr term))))
            (and (not (negative-syntaxp (cadr term)))
              (negative-syntaxp (caddr term))))))
      (otherwise nil))))