		Search-engine friendly clone of the ACL2 documentation.

Stv-extraction-alists

Stv-nth-extraction-alist

Add the bindings for name to entryN to the NTH-ALIST-ACC

Signature
(stv-nth-extraction-alist n lines nth-alist-acc) → *
Arguments: n — Guard (natp n).; lines — A list of (name entry1 ... entryK).
Guard (true-list-listp lines).; nth-alist-acc — Guard (alistp nth-alist-acc).

Definitions and Theorems

Function: stv-nth-extraction-alist

(defun stv-nth-extraction-alist (n lines nth-alist-acc)
  (declare (xargs :guard (and (natp n)
                              (true-list-listp lines)
                              (alistp nth-alist-acc))))
  (let ((__function__ 'stv-nth-extraction-alist))
    (declare (ignorable __function__))
    (b* (((when (atom lines)) nth-alist-acc)
         (line1 (car lines))
         ((cons name entries) line1)
         (entry (nth n entries))
         ((when (eq entry '_))
          (stv-nth-extraction-alist n (cdr lines)
                                    nth-alist-acc))
         (nth-alist-acc
              (safe-pairlis-onto-acc name entry nth-alist-acc)))
      (stv-nth-extraction-alist n (cdr lines)
                                nth-alist-acc))))