		Search-engine friendly clone of the ACL2 documentation.

Paired-name-separator

Get-paired-name-separator

Retrieve the current separator for paired names.

Signature
(get-paired-name-separator wrld) → separator
Arguments: wrld — Guard (plist-worldp wrld).
Returns: separator — A paired-name-separator-p.

If the separator is not set yet, the default is returned.

Definitions and Theorems

Function: get-paired-name-separator

(defun get-paired-name-separator (wrld)
  (declare (xargs :guard (plist-worldp wrld)))
  (let ((__function__ 'get-paired-name-separator))
    (declare (ignorable __function__))
    (let ((pair (assoc-eq 'separator
                          (table-alist 'paired-name-separator
                                       wrld))))
      (if pair (cdr pair)
        *default-paired-name-separator*))))