►Dracula: Reference Manual
▼1 ACL2
►1.6 ACL2 Books
On this page:
1.6.1 "data-structures/ list-theory"
deflist
1.6.2 "data-structures/ structures"
defstructure
  ← prev  up  next → 

1.6 ACL2 Books

1.6.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)

  rename-below: used outside of begin-below in: (rename-below

  (even-listp12 even-listp1))

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

  compile: unbound identifier (and no #%top syntax

  transformer is bound) in: even-listp1

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

  compile: unbound identifier (and no #%top syntax

  transformer is bound) in: even-listp1

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

  compile: unbound identifier (and no #%top syntax

  transformer is bound) in: even-listp1

1.6.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)

  rename-below: used outside of begin-below in: (rename-below

  (circle49 circle4))

  > (circle 10)

  eval:6:0: circle: undefined in: circle

  > (circle-radius (circle 10))

  eval:7:0: circle-radius: undefined in: circle-radius

  > (circle-p (circle 10))

  eval:8:0: circle-p: undefined in: circle-p

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

  eval:9:0: circle-p: undefined in: circle-p

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

  rename-below: used outside of begin-below in: (rename-below

  (rect1218 rect12))

  > (rect 10 20)

  eval:11:0: rect: undefined in: rect

  > (rect-width (rect 10 20))

  eval:12:0: rect-width: undefined in: rect-width

  > (rect-height (rect 10 20))

  eval:13:0: rect-height: undefined in: rect-height

  > (rect-p (rect 10 20))

  eval:14:0: rect-p: undefined in: rect-p

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

  eval:15:0: rect-p: undefined in: rect-p

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

  eval:16:0: rect-p: undefined in: rect-p

  ← prev  up  next →