		Search-engine friendly clone of the ACL2 documentation.

Schemalg-input-processing

Schemalg-process-fvar-1-name

Process the :fvar-1-name input.

Signature
(schemalg-process-fvar-1-name fvar-1-name ?f acl2::names-to-avoid ctx state) → (mv acl2::erp acl2::result state)
Arguments: ?f — Guard (symbolp ?f).; 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-fvar-1-name

(defun schemalg-process-fvar-1-name
       (fvar-1-name ?f acl2::names-to-avoid ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp ?f)
                             (symbol-listp acl2::names-to-avoid))))
 (let ((__function__ 'schemalg-process-fvar-1-name))
  (declare (ignorable __function__))
  (b*
   (((er &)
     (ensure-value-is-symbol$ fvar-1-name
                              (msg "The ~x0 input" :fvar-1-name)
                              t nil))
    (acl2::fn (if (eq fvar-1-name :auto)
                  (add-suffix ?f "-1")
                fvar-1-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 :fvar-1-name)
      'function
      acl2::names-to-avoid t nil)))
   (value (list acl2::fn acl2::names-to-avoid)))))