Tailrec-gen-var-u
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-u old$) → u
- Arguments
- old$ — Guard (symbolp old$).
- Returns
- u — A symbolp.
Definitions and Theorems
Function: tailrec-gen-var-u
(defun tailrec-gen-var-u (old$)
(declare (xargs :guard (symbolp old$)))
(let ((__function__ 'tailrec-gen-var-u))
(declare (ignorable __function__))
(genvar old$ "U" nil nil)))
