		Search-engine friendly clone of the ACL2 documentation.

Tailrec-event-generation

Tailrec-gen-combine-op

Generate the combination operator.

Signature
(tailrec-gen-combine-op combine q r) → combine-op
Arguments: combine — Guard (pseudo-termp combine).; q — Guard (symbolp q).; r — Guard (symbolp r).
Returns: combine-op — Type (pseudo-lambdap combine-op), given the guard.

This is obtained by abstracting combine<q,r> over q and r.

Definitions and Theorems

Function: tailrec-gen-combine-op

(defun tailrec-gen-combine-op (combine q r)
  (declare (xargs :guard (and (pseudo-termp combine)
                              (symbolp q)
                              (symbolp r))))
  (let ((__function__ 'tailrec-gen-combine-op))
    (declare (ignorable __function__))
    (make-lambda (list q r) combine)))

Theorem: pseudo-lambdap-of-tailrec-gen-combine-op

(defthm pseudo-lambdap-of-tailrec-gen-combine-op
  (implies (and (pseudo-termp combine)
                (symbolp q)
                (symbolp r))
           (b* ((combine-op (tailrec-gen-combine-op combine q r)))
             (pseudo-lambdap combine-op)))
  :rule-classes :rewrite)