		Search-engine friendly clone of the ACL2 documentation.

Pure-expression-execution

Induct-exec-expr-list-of-pure

Induction scheme for exec-expr-list applied to a list of pure expressions.

Signature
(induct-exec-expr-list-of-pure exprs limit) → *
Arguments: exprs — Guard (expr-listp exprs).; limit — Guard (natp limit).

This concerns both the list structure and the limit.

Definitions and Theorems

Function: induct-exec-expr-list-of-pure

(defun induct-exec-expr-list-of-pure (exprs limit)
  (declare (xargs :guard (and (expr-listp exprs) (natp limit))))
  (cond ((endp exprs) nil)
        (t (induct-exec-expr-list-of-pure (cdr exprs)
                                          (1- limit)))))