		Search-engine friendly clone of the ACL2 documentation.

List-utilities

Some utilities for lists.

These are for lists with elements of any types, similarly to std/lists. In contrast, the typed list utilities are for lists with elements of homogeneous types.

These utilities may be eventually integrated into std/lists.

Subtopics

Set-size: Size of a set represented as a list.
List-len-const-theorems: Some theorems about lists whose lengths are (i) equal, (ii) equal or above, or (iii) above constant values.
Nthcdr-theorems: Some theorems about the built-in function nthcdr.
Append-theorems: Some theorems about the built-in function append.
Rev-theorems: Some theorems about the library function rev.
Prefixp-theorems: Some theorems about the library function prefixp.
Take-theorems: Some theorems about the built-in function take.
Intersectp-equal-theorems: Some theorems about the built-in function intersectp.
List-primitive-theorems: Some theorems about the list primitive functions (i.e. car, cdr, cons, and consp).
Set-difference-equal-theorems: Some theorems about the built-in function set-difference$.
Intersection-equal-theorems: Some theorems about the built-in function intersection$.
Index-of-theorems: Some theorems about the library function index-of.
Last-theorems: Some theorems about the built-in function last.