		Search-engine friendly clone of the ACL2 documentation.

Defunit

Generate a singleton fixtype.

Introduction

Some languages have a unit type, which consists of a single value. This is useful, for example, when some code returns nothing (besides presumably having some side effects), or as a component of larger types (e.g. a disjoint union of a detailed error value for failure and of the unit type for success without further information).

This macro introduces a fixtype consisting of a single keyword value. Given that ACL2 is an untyped language, the ability to customize the exact value of a unit type provides more flexibility, e.g. to create flat sums involving unit types, which requires such unit types to be disjoint from the other summand types, which are unknown a priori.

General Form

(defunit type
         :value ...    ; no default
         :pred ...     ; default type-p
         :fix ...      ; default type-fix
         :equiv ...    ; default type-equiv
         :parents ...  ; no default
         :short ...    ; no default
         :long ...     ; no default
  )

Inputs

type

The name of the new fixtype.

:value — no default

A keyword to be used as the (only) value of the new fixtype.
This must be provided, there is no default.

:parents — default type followed by -p
:short — default type followed by -fix
:long — default type followed by -equiv

The name of the recognizer, fixer, and equivalence for the new fixtype.

:parents — no default
:short — no default
:long — no default

The parents, short string, and long string for the XDOC topic generated for the new fixtype.
If any of these is not supplied, it is omitted from the XDOC topic; there are no defaults.

Generated Events

The following are generated, inclusive of XDOC documentation:

The recognizer, the fixer, the equivalence, and the fixtype.

See the implementation, which uses a readable backquote notation, for details.

Subtopics

Defunit-implementation: Implementation of defunit.