		Search-engine friendly clone of the ACL2 documentation.

Defarbrec-event-generation

Defarbrec-gen-var-k

Generate the variable k that counts the iterated updates of the arguments.

Signature
(defarbrec-gen-var-k fn$ x1...xn$) → k
Arguments: fn$ — Guard (symbolp fn$).; x1...xn$ — Guard (symbol-listp x1...xn$).
Returns: k — A symbolp.

This is used as a formal parameter of the iterated argument update functions, the bound variable in the termination testing predicate, and a formal parameter of the measure function. This variable must be distinct from the formal parameters of fn.

Definitions and Theorems

Function: defarbrec-gen-var-k

(defun defarbrec-gen-var-k (fn$ x1...xn$)
  (declare (xargs :guard (and (symbolp fn$)
                              (symbol-listp x1...xn$))))
  (let ((__function__ 'defarbrec-gen-var-k))
    (declare (ignorable __function__))
    (genvar fn$ "K" nil x1...xn$)))