|
|
|---|
|
|
|
|---|
Define a simple for-loop-style iteration, counting up over some range.
This macro defines the logic version of this loop as a non-tail-recursive function that counts down from the maximum value to the minimum value. This is often better for reasoning with. The executable version is a function that counts up from the minimum to the maximum value and is tail-recursive, which may be better for execution, especially in terms of avoiding stack overflows.
Syntax:
(defiteration function-name (a b c) "optional doc string" (declare ...) ;; optional declare forms (body idx-var a b c) ;; one step of the iteration :returns (mv b c) ;; or a single variable, must be from the formals :index idx-var ;; counter variable :first (foo a b) ;; starting index, default 0 :last (bar a c) ;; final index :hints ... ;; optional, for proving that tailrec and non-tailrec ;; are the same :guard-hints ... ;; for defining the step function :package foo) ;; package witness symbol, default is function-name