		Search-engine friendly clone of the ACL2 documentation.

Defarbrec-event-generation

Defarbrec-gen-var-l

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

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

This is used in one of the generated local lemmas about the measure function. This variable must be distinct from the formal parameters of fn as well as from the variable k.

Definitions and Theorems

Function: defarbrec-gen-var-l

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