		Search-engine friendly clone of the ACL2 documentation.

Schemalg-input-processing

Schemalg-process-equal-algo-name

Process the :equal-algo-name input.

Signature
(schemalg-process-equal-algo-name equal-algo-name ?f algo acl2::names-to-avoid ctx state) → (mv acl2::erp acl2::result state)
Arguments: ?f — Guard (symbolp ?f).; algo — Guard (symbolp algo).; acl2::names-to-avoid — Guard (symbol-listp acl2::names-to-avoid).
Returns: acl2::result — A (tuple (fn symbolp) (updated-names-to-avoid symbol-listp) result).

Definitions and Theorems

Function: schemalg-process-equal-algo-name

(defun schemalg-process-equal-algo-name
       (equal-algo-name ?f algo acl2::names-to-avoid ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp ?f)
                             (symbolp algo)
                             (symbol-listp acl2::names-to-avoid))))
 (let ((__function__ 'schemalg-process-equal-algo-name))
  (declare (ignorable __function__))
  (b*
   (((er &)
     (ensure-value-is-symbol$ equal-algo-name
                              (msg "The ~x0 input" :equal-algo-name)
                              t nil))
    (acl2::fn (if (eq equal-algo-name :auto)
                  (packn-pos (list "EQUAL[" ?f "][" algo "]")
                             ?f)
                equal-algo-name))
    ((er acl2::names-to-avoid)
     (ensure-symbol-is-fresh-event-name$
      acl2::fn
      (msg
       "The name ~x0 specified (perhaps by default) by the ~x1 input"
       acl2::fn :equal-algo-name)
      'function
      acl2::names-to-avoid t nil)))
   (value (list acl2::fn acl2::names-to-avoid)))))