		Search-engine friendly clone of the ACL2 documentation.

Defoption

Define an option type.

defoption generates a recognizer predicate and fixing function for a new type whose elements either belong to the argument type or are nil. This is analogous to the "option" or "maybe" types of various other languages, except that defoption types are untagged. In order to distinguish the nil case from the argument type, the recognizer for the argument type must not admit nil.

defoption is compatible with deftypes and can be mutually-recursive with other deftypes-compatible type generators.

The syntax of defoption is:

(defoption foo-option
  foo                  ;; type argument
  :parents (...)       ;; xdoc
  :short "..."         ;; xdoc
  :long "..."          ;; xdoc
  :measure (+ 1 (* 2 (acl2-count x)))
                       ;; default: (acl2-count x)
  :xvar x              ;; default: x, or find x symbol in measure
  :prepwork            ;; admit these events before starting
  :pred foo?-p         ;; default: foo-option-p
  :fix foo?-fix        ;; default: foo-option-fix
  :equiv foo?-=        ;; default: foo-option-equiv
  :case  foo?-case     ;; default: foo-option-case
  :count foo?-cnt      ;; default: foo-option-count
                       ;; (may be nil; skipped unless mutually recursive)
  :inline (:kind :fix) ;; default: (:kind :fix :acc)
  )

Note that the type argument must precede any keyword arguments.