Filtering...

enumerations

books/kestrel/utilities/enumerations

Included Books

defenum
other
(in-package "ACL2")
include-book
(include-book "std/util/defenum" :dir :system)
other
(defxdoc miscellaneous-enumerations
  :parents (kestrel-utilities)
  :short "Some miscellaneous enumerations.")
other
(defenum logic/program-p
  (:logic :program)
  :parents (miscellaneous-enumerations)
  :short "Enumeration of @(see defun-mode)s.")
other
(defenum logic/program/auto-p
  (:logic :program :auto)
  :parents (miscellaneous-enumerations)
  :short "Enumeration of @(see defun-mode)s and @(':auto').")
other
(defenum t/nil/auto-p
  (t nil :auto)
  :parents (miscellaneous-enumerations)
  :short "Enumeration of booleans and @(':auto').")