• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
    • Defunc
    • Fty
      • Deftagsum
      • Defprod
      • Defflexsum
      • Defbitstruct
      • Deflist
      • Defalist
      • Defbyte
      • Deffixequiv
      • Defresult
      • Deffixtype
      • Fty-discipline
      • Defoption
      • Fty-extensions
      • Defsubtype
      • Defset
        • Defset-implementation
      • Specific-types
      • Deftypes
      • Defflatsum
      • Deflist-of-len
      • Defbytelist
      • Fty::basetypes
      • Defvisitors
      • Defomap
      • Deffixtype-alias
      • Deffixequiv-sk
      • Defunit
      • Deffixequiv-mutual
      • Fty::baselists
      • Defmap
    • Apt
    • Std/util
    • Defdata
    • Defrstobj
    • Seq
    • Match-tree
    • Defrstobj
    • With-supporters
    • Def-partial-measure
    • Template-subst
    • Soft
    • Defthm-domain
    • Event-macros
    • Def-universal-equiv
    • Def-saved-obligs
    • With-supporters-after
    • Definec
    • Sig
    • Outer-local
    • Data-structures
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Fty-extensions
• Fty
• Std/osets

Defset

Generate a fixtype of osets whose elements have a specified fixtype.

Introduction

This is analogous to deflist, defalist, and defomap. Besides the fixtype itself, this macro also generates some theorems about the fixtype. Future versions of this macro may generate more theorems, as needed.

Aside from the recognizer, fixer, and equivalence for the fixtype, this macro does not generate any operations on the typed osets. Instead, the generic oset operations can be used on typed osets. This macro generates theorems about the use of these generic operations on typed osets.

Future versions of this macro may be modularized to provide a ``sub-macro'' that generates only the recognizer and theorems about it, without the fixtype (and without the fixer and equivalence), similarly to std::deflist and std::defalist. That sub-macro could be called set::defset.

General Form

(defset type
        :elt-type ...
        :elementp-of-nil ...
        :pred ...
        :fix ...
        :equiv ...
        :measure ...
        :parents ...
        :short ...
        :long ...
  )

Inputs

type

The name of the new fixtype.

:elt-type

The (existing) fixtype of the elements of the new set fixtype.

:elementp-of-nil

Specifies whether nil is in the element fixtype :elt-type. It must be t, nil, or :unknown (the default). When t or nil, slightly better theorems are generated.

:pred
:fix
:equiv

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

The defaults are type followed by -p, -fix, and -equiv.

:parents
:short
:long

These are used to generate XDOC documentation for the topic name.

If any of these is not supplied, the corresponding component is omitted from the generated XDOC topic.

This macro currently does not perform a thorough validation of its inputs. Erroneous inputs may result in failures of the generated events. Errors should be easy to diagnose, also since this macro has a very simple and readable implementation. Future versions of this macro should perform more thorough input validation.

Generated Events

The following are generated, inclusive of XDOC documentation:

• The recognizer, the fixer, the equivalence, and the fixtype.
• Several theorems about the recognizer, fixer, and equivalence.

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

Subtopics

Defset-implementation

Implementation of defset.