		Search-engine friendly clone of the ACL2 documentation.

Tailrec-event-generation

Tailrec-gen-id-var-u

Generate the variable u to use in the :combine-left-identity and :combine-right-identity applicability conditions.

Signature
(tailrec-gen-id-var-u old$ wrld) → u
Arguments: old$ — Guard (symbolp old$).; wrld — Guard (plist-worldp wrld).
Returns: u — A symbolp.

This must be distinct from the formals of the old function.

Definitions and Theorems

Function: tailrec-gen-id-var-u

(defun tailrec-gen-id-var-u (old$ wrld)
  (declare (xargs :guard (and (symbolp old$)
                              (plist-worldp wrld))))
  (let ((__function__ 'tailrec-gen-id-var-u))
    (declare (ignorable __function__))
    (genvar old$ "U" nil (formals old$ wrld))))