		Search-engine friendly clone of the ACL2 documentation.

Programming

Def-list-constructor

Define function that constructs a list, just by giving the length and how to compute the Nth element in terms of the formals and index.

This takes many of the same arguments as defiteration, and in fact it uses defiteration. But instead of giving the step function for the iteration, you give the value of the Nth element of the list. You must also provide the keyword :last, giving the length of the list.

What you end up with is your top-level function, definition disabled, and four rules:

nth-of-fnname tells what the Nth element is, for N in bounds
nth-of-fnname-split (disabled), tells what the Nth element is, causing a case-split on whether it's in bounds or not
len-of-fnname: gives the length of the list
true-listp-of-fnname shows that the list is true-listp.

See centaur/misc/equal-by-nths for a strategy that proves equivalences between lists based on length and Nth value.

Syntax:

(def-list-constructor foo (x y)
  "optional doc string"
  (declare (xargs ...))   ;; optional declare forms
  (+ idx-var x y)         ;; value of the IDX-VARth element
  :length  (bar x y)      ;; final index
  :index idx-var          ;; counter variable, default N
  ... defiteration args ...)