		Search-engine friendly clone of the ACL2 documentation.

Defequal-event-generation

Defequal-gen-equality

Generate the equality function.

Signature
(defequal-gen-equality name left right x1...xn enable verify-guards left-to-right left-to-right-enable) → (mv local-event exported-event)
Arguments: name — Guard (symbolp name).; left — Guard (symbolp left).; right — Guard (symbolp right).; x1...xn — Guard (symbol-listp x1...xn).; enable — Guard (booleanp enable).; verify-guards — Guard (booleanp verify-guards).; left-to-right — Guard (symbolp left-to-right).
Returns: local-event — Type (pseudo-event-formp local-event).; exported-event — Type (pseudo-event-formp exported-event).

Definitions and Theorems

Function: defequal-gen-equality

(defun defequal-gen-equality
       (name left right x1...xn enable verify-guards
             left-to-right left-to-right-enable)
 (declare (xargs :guard (and (symbolp name)
                             (symbolp left)
                             (symbolp right)
                             (symbol-listp x1...xn)
                             (booleanp enable)
                             (booleanp verify-guards)
                             (symbolp left-to-right))))
 (let ((__function__ 'defequal-gen-equality))
  (declare (ignorable __function__))
  (b*
   ((macro (if enable 'defun-sk2 'defund-sk2))
    (body
     (cons
          'forall
          (cons x1...xn
                (cons (cons 'equal
                            (cons (cons left x1...xn)
                                  (cons (cons right x1...xn) 'nil)))
                      'nil))))
    (declare
     (cons
         'declare
         (cons (cons 'xargs
                     (cons ':guard
                           (cons 't
                                 (cons ':verify-guards
                                       (cons verify-guards 'nil)))))
               'nil)))
    (options (cons ':rewrite
                   (cons ':direct
                         (cons ':thm-name
                               (cons left-to-right
                                     (and (not enable)
                                          left-to-right-enable
                                          (list :thm-enable t)))))))
    (local-event
     (cons
      'local
      (cons
       (cons
        macro
        (cons
         name
         (cons
          'nil
          (cons
           declare
           (append
            (and
             verify-guards
             '((declare
                   (xargs :guard-hints (("Goal" :in-theory nil))))))
            (cons body options))))))
       'nil)))
    (exported-event
         (cons macro
               (cons name
                     (cons 'nil
                           (cons declare (cons body options)))))))
   (mv local-event exported-event))))

Theorem: pseudo-event-formp-of-defequal-gen-equality.local-event

(defthm pseudo-event-formp-of-defequal-gen-equality.local-event
  (b*
    (((mv ?local-event ?exported-event)
      (defequal-gen-equality name
                             left right x1...xn enable verify-guards
                             left-to-right left-to-right-enable)))
    (pseudo-event-formp local-event))
  :rule-classes :rewrite)

Theorem: pseudo-event-formp-of-defequal-gen-equality.exported-event

(defthm pseudo-event-formp-of-defequal-gen-equality.exported-event
  (b*
    (((mv ?local-event ?exported-event)
      (defequal-gen-equality name
                             left right x1...xn enable verify-guards
                             left-to-right left-to-right-enable)))
    (pseudo-event-formp exported-event))
  :rule-classes :rewrite)