		Search-engine friendly clone of the ACL2 documentation.

Schemalg-input-processing

Schemalg-process-algo-name-aux

Signature
(schemalg-process-algo-name-aux ?f1...?fp) → [?f1]...[?fp]-chars
Arguments: ?f1...?fp — Guard (symbol-listp ?f1...?fp).

Definitions and Theorems

Function: schemalg-process-algo-name-aux

(defun schemalg-process-algo-name-aux (?f1...?fp)
 (declare (xargs :guard (symbol-listp ?f1...?fp)))
 (let ((__function__ 'schemalg-process-algo-name-aux))
  (declare (ignorable __function__))
  (cond
    ((endp ?f1...?fp) nil)
    (t (append (list #\[)
               (explode (symbol-name (car ?f1...?fp)))
               (list #\])
               (schemalg-process-algo-name-aux (cdr ?f1...?fp)))))))