		Search-engine friendly clone of the ACL2 documentation.

Deffixequiv-sk-implementation

Deffixequiv-sk-fn

Process the inputs and generate the deffixequiv.

Signature
(deffixequiv-sk-fn fn args wrld) → event
Arguments: wrld — Guard (plist-worldp wrld).
Returns: event — A ACL2::maybe-pseudo-event-formp.

Definitions and Theorems

Function: deffixequiv-sk-fn

(defun deffixequiv-sk-fn (fn args wrld)
 (declare (xargs :guard (plist-worldp wrld)))
 (let ((__function__ 'deffixequiv-sk-fn))
  (declare (ignorable __function__))
  (b*
   (((unless (acl2::defun-sk-namep fn wrld))
     (raise
         "The first input, ~x0, must be a DEFUN-SK function symbol."
         fn))
    (fn-rule (acl2::defun-sk-rewrite-name fn wrld))
    (fn-witness (acl2::defun-sk-witness fn wrld))
    (bvars (acl2::defun-sk-bound-vars fn wrld))
    ((unless (doublet-listp args))
     (raise "The :ARGS input, ~x0, must be a true list of doublets."
            args))
    (args-alist (acl2::doublets-to-alist args))
    ((unless (acl2::symbol-symbol-alistp args-alist))
     (raise
      "The :ARGS input, ~x0, ~
                must be a true list of doublets of symbols."
      args))
    (hints (deffixequiv-sk-hints fn fn-rule
                                 fn-witness bvars args-alist wrld)))
   (cons 'deffixequiv
         (cons fn
               (cons ':args
                     (cons args
                           (cons ':hints (cons hints 'nil)))))))))