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