		Search-engine friendly clone of the ACL2 documentation.

Schemalg-event-generation

Schemalg-gen-equal-algo

Generate the function equal[?f][algo[?f1]...[?fp]].

Signature
(schemalg-gen-equal-algo equal-algo equal-algo-enable vars ?f algo print) → event
Arguments: equal-algo — Guard (symbolp equal-algo).; equal-algo-enable — Guard (booleanp equal-algo-enable).; vars — Guard (symbol-listp vars).; ?f — Guard (symbolp ?f).; algo — Guard (symbolp algo).; print — Guard (evmac-input-print-p print).
Returns: event — Type (pseudo-event-formp event).

Unless the :print input of schemalg is :all, we pass :print nil to soft::defequal, to avoid showing its expansion on the screen (see soft::defequal). Instead, the code in schemalg-gen-everything shows the soft::defequal form itself (if schemalg's :print is at least :result).

We do not expect this soft::defequal event to fail (it would be an internal/implementation error if it did). So there is no need to pass :print :error. If the event actually fails, then it can be debugged by passing :all to schemalg, which in this cases also passes it to equal, or by passing :show-only t to schemalg and examining/trying the resulting expansion.

Definitions and Theorems

Function: schemalg-gen-equal-algo

(defun schemalg-gen-equal-algo
       (equal-algo equal-algo-enable vars ?f algo print)
 (declare (xargs :guard (and (symbolp equal-algo)
                             (booleanp equal-algo-enable)
                             (symbol-listp vars)
                             (symbolp ?f)
                             (symbolp algo)
                             (evmac-input-print-p print))))
 (let ((__function__ 'schemalg-gen-equal-algo))
  (declare (ignorable __function__))
  (cons
   'soft::defequal
   (cons
    equal-algo
    (cons
     ':left
     (cons
      ?f
      (cons
       ':right
       (cons
        algo
        (cons
         ':vars
         (cons
          vars
          (cons
           ':enable
           (cons
            equal-algo-enable
            (cons
             ':left-to-right-enable
             (cons
                  equal-algo-enable
                  (cons ':right-to-left-enable
                        (cons equal-algo-enable
                              (cons ':print
                                    (cons (and (eq print :all) :all)
                                          'nil))))))))))))))))))

Theorem: pseudo-event-formp-of-schemalg-gen-equal-algo

(defthm pseudo-event-formp-of-schemalg-gen-equal-algo
 (b*
  ((event
    (schemalg-gen-equal-algo equal-algo
                             equal-algo-enable vars ?f algo print)))
  (pseudo-event-formp event))
 :rule-classes :rewrite)