		Search-engine friendly clone of the ACL2 documentation.

Register-type

Example

(defun nth-odd-builtin (n) 
  (if (evenp n)
      (1+ n)
    (- n)))

(register-type odd
               :predicate oddp 
               :enumerator nth-odd-builtin)

Introduction

A defdata type expression can either be a typename, a quoted constant or a combinator or constructor expression. To serve as a typename, a symbol should either have been defined using the defdata macro, or it should have been registered as a defdata type using the register-type macro.

As an example, after having registered odd above, we can now use odd to define other defdata types, e.g., a list of odd numbers:

(defdata odds (listof odd))

General Form:

(register-type name
               :predicate pred
               :enumerator enum
               [:enum/acc enum2]
               [:enum/test tenum]
               [:enum/test/acc tenum2]
               [:clique tnames]
               [:normalized-def nexp]
               [:prettyified-def pexp]
               ...)

Consider the above call of register-type. We expect the following guards to be satisfied.

pred is a monadic boolean-valued function.
enum, tenum are 1-arity functions that take a natural number and return a value of the right type.
enum2, tenum2 are 2-arity functions that take a natural number and a random seed and return (mv value seed).
The rest of the options are for experts and are not yet documented.