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.

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