(tailrec-gen-alpha-component-terms-aux i alpha-name formals terms) → final-terms
Function:
(defun tailrec-gen-alpha-component-terms-aux (i alpha-name formals terms) (declare (xargs :guard (and (natp i) (symbolp alpha-name) (symbol-listp formals) (pseudo-term-listp terms)))) (let ((__function__ 'tailrec-gen-alpha-component-terms-aux)) (declare (ignorable __function__)) (if (zp i) terms (b* ((i-1 (1- i)) (term (cons 'nth (cons (cons 'quote (cons i-1 'nil)) (cons (cons alpha-name formals) 'nil))))) (tailrec-gen-alpha-component-terms-aux i-1 alpha-name formals (cons term terms))))))