Tailrec-gen-var-w
Generate the variable u to use in the
:combine-associativity and
:combine-associativity-uncond
applicability conditions.
- Signature
(tailrec-gen-var-w old$) → w
- Arguments
- old$ — Guard (symbolp old$).
- Returns
- w — A symbolp.
Definitions and Theorems
Function: tailrec-gen-var-w
(defun tailrec-gen-var-w (old$)
(declare (xargs :guard (symbolp old$)))
(let ((__function__ 'tailrec-gen-var-w))
(declare (ignorable __function__))
(genvar old$ "W" nil nil)))
