Process the
(schemalg-process-spec-1-name spec-1-name old ?h/?g2 acl2::names-to-avoid ctx state) → (mv acl2::erp acl2::result state)
Function:
(defun schemalg-process-spec-1-name (spec-1-name old ?h/?g2 acl2::names-to-avoid ctx state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (symbolp old) (symbolp ?h/?g2) (symbol-listp acl2::names-to-avoid)))) (let ((__function__ 'schemalg-process-spec-1-name)) (declare (ignorable __function__)) (b* (((er &) (ensure-value-is-symbol$ spec-1-name (msg "The ~x0 input" :spec-1-name) t nil)) (acl2::fn (if (eq spec-1-name :auto) (packn-pos (list old "-1" "[" ?h/?g2 "]") old) spec-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 :spec-1-name) 'function acl2::names-to-avoid t nil))) (value (list acl2::fn acl2::names-to-avoid)))))