3.1 ACL2 Books

3.1.1 "data-structures/list-theory"

(include-book "data-structures/list-theory" :dir :system)

(deflist <list-pred> (l) <pred>)

Dracula supports the deflist form for defining new list types from the "data-structures/list-theory" book. It defines the predicate <list-pred>, recognizing lists whose elements satisfy <pred>. The (l) identifies the list as the predicate’s only parameter; ACL2 supports other parameter lists but Dracula currently does not.

Examples:

> (deflist even-listp (l) evenp)

> (even-listp (list 2 4 6))

t

> (even-listp (list 1 3 5))

()

> (even-listp 'not-a-list)

()

3.1.2 "data-structures/structures"

(include-book "data-structures/structures" :dir :system)

(defstructure <name> field ...)   field   =   <field-name>     |   (<field-name> (:assert <guard-expr>))

Dracula supports the defstructure form for defining new structure types from the "data-structures/structures" book. It defines a constructor <name>, a predicate <name>-p a weak predicate weak-<name>-p, and a selector <name>-<field-name> for each field, with optional guards for the structure and each field which are incorporated into the predicate (but not the weak predicate).

Examples:

> (defstructure circle radius)

> (circle 10)

(circle 10)

> (circle-radius (circle 10))

10

> (circle-p (circle 10))

t

> (circle-p 'not-a-circle)

()

> (defstructure rect       (width (:assert (natp width)))       (height (:assert (natp height))))

> (rect 10 20)

(rect 10 20)

> (rect-width (rect 10 20))

10

> (rect-height (rect 10 20))

20

> (rect-p (rect 10 20))

t

> (rect-p (rect -10 -20))

()

> (rect-p 'not-a-rect)

()