		Search-engine friendly clone of the ACL2 documentation.

Defequal-input-processing

Defequal-process-left-and-right

Process the :left and :right inputs.

Signature
(defequal-process-left-and-right left left-present right right-present verify-guards ctx state) → (mv erp n state)
Arguments: left-present — Guard (booleanp left-present).; right-present — Guard (booleanp right-present).
Returns: n — Type (natp n).

Definitions and Theorems

Function: defequal-process-left-and-right

(defun defequal-process-left-and-right
       (left left-present right
             right-present verify-guards ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (booleanp left-present)
                             (booleanp right-present))))
 (let ((__function__ 'defequal-process-left-and-right))
  (declare (ignorable __function__))
  (b*
   ((wrld (w state))
    ((unless left-present)
     (er-soft+ ctx t 0
               "The :LEFT input must be present, but it is not."))
    ((unless right-present)
     (er-soft+ ctx t 0
               "The :RIGHT input must be present, but it is not."))
    ((er &)
     (ensure-value-is-function-name$
          left (msg "The :LEFT input ~x0" left)
          t 0))
    ((er &)
     (ensure-value-is-function-name$
          right (msg "The :RIGHT input ~x0" right)
          t 0))
    (left-guard (uguard left wrld))
    (right-guard (uguard right wrld))
    (left-arity (arity+ left wrld))
    (right-arity (arity+ right wrld))
    ((unless (= left-arity right-arity))
     (er-soft+
      ctx t 0
      "The function ~x0 specified by the :LEFT input ~
                   and the function ~x1 specified by :RIGHT input ~
                   must have the same arity, but they do not: ~
                   the first has arity ~x2 and the second has arity ~x3."
      left right left-arity right-arity))
    ((unless (> left-arity 0))
     (er-soft+
      ctx t 0
      "The arity of the functions ~x0 and ~x1 ~
                   specified by the :LEFT and :RIGHT inputs ~
                   must not be zero, but it is zero instead."
      left right))
    ((when (and (not (funvarp left wrld))
                (not (sofunp left wrld))
                (not (funvarp right wrld))
                (not (sofunp right wrld))))
     (er-soft+
      ctx t 0
      "At least one of the two functions ~x0 and ~x1 ~
                   specified by the :LEFT and :RIGHT inputs ~
                   must be a function variable ~
                   or a second-order function, ~
                   but they are not."
      left right))
    ((er &)
     (if
      (eq verify-guards t)
      (b*
       (((unless (equal left-guard *t*))
         (er-soft+
          ctx t 0
          "Since the :VERIFY-GUARD input ~
                             is (perhaps by default) T, ~
                             the guard of the function ~x0 ~
                             specified by the :LEFT input ~
                             must be T, but it is ~x1 instead."
          left left-guard))
        ((unless (equal right-guard *t*))
         (er-soft+
          ctx t 0
          "Since the :VERIFY-GUARD input ~
                             is (perhaps by default) T, ~
                             the guard of the function ~x0 ~
                             specified by the :RIGHT input ~
                             must be T, but it is ~x1 instead."
          right right-guard))
        ((unless (guard-verified-p+ left wrld))
         (er-soft+
          ctx t 0
          "Since the :VERIFY-GUARD input ~
                             is (perhaps by default) T, ~
                             the function ~x0 ~
                             specified by the :LEFT input ~
                             must be guard-verified, but it is not."
          left))
        ((unless (guard-verified-p+ right wrld))
         (er-soft+
          ctx t 0
          "Since the :VERIFY-GUARD input ~
                             is (perhaps by default) T, ~
                             the function ~x0 ~
                             specified by the :RIGHT input ~
                             must be guard-verified, but it is not."
          right)))
       (value nil))
      (value nil))))
   (value left-arity))))

Theorem: natp-of-defequal-process-left-and-right.n

(defthm natp-of-defequal-process-left-and-right.n
  (b* (((mv ?erp ?n acl2::?state)
        (defequal-process-left-and-right
             left left-present right
             right-present verify-guards ctx state)))
    (natp n))
  :rule-classes :rewrite)