		Search-engine friendly clone of the ACL2 documentation.

Acre-internals

Captures-bindings

Signature
(captures-bindings args index matchresult !) → *

Definitions and Theorems

Function: captures-bindings

(defun captures-bindings (args index matchresult !)
 (declare (xargs :guard t))
 (let ((__function__ 'captures-bindings))
  (declare (ignorable __function__))
  (b*
   (((when (atom args)) nil)
    (arg (car args))
    (fn (if ! 'matchresult->captured-substr!
          'matchresult->captured-substr))
    ((when (symbolp arg))
     (cons
          (cons arg
                (cons (cons fn (cons index (cons matchresult 'nil)))
                      'nil))
          (captures-bindings (cdr args)
                             (+ 1 index)
                             matchresult !))))
   (case-match arg
    ((var name)
     (cons (cons var
                 (cons (cons fn (cons name (cons matchresult 'nil)))
                       'nil))
           (captures-bindings (cdr args)
                              (+ 1 index)
                              matchresult !)))
    (& (er hard? 'captures-bindings
           "Bad capture element: ~x0" arg))))))