		Search-engine friendly clone of the ACL2 documentation.

Def-enumcase

Introduce a case macro for an enum type, compatible with multicase

Usage:

(def-enumcase myenum-case myenum-p)

This defines a typesafe case macro myenum-case which can be used on myenum-p objects, assuming that myenum-p is an enumeration type defined using std::defenum. This macro can be used with multicase. An example of its regular usage is as follows:

(std::defenum myenum-p (:a :b :c :d))

(def-enumcase myenum-case myenum-p)

;; check that x equals :c
(myenum-case x :c)

;; translation error: :e is not one of the possibilities
(myenum-case x :e)

;; check that x is one of :a, :c
(myenum-case x '(:a :c))

;; translation error -- :e is not of the possibilities
(myenum-case x '(:a :e))

;; regular case statement usage
(myenum-case x
   :a "alpha"
   :b "beta"
   :c "kappa"
   :d "delta")

;; another form of the above
(myenum-case x
   (:a "alpha")
   (:b "beta")
   (:c "kappa")
   (:d "delta"))

;; case statement with default
(myenum-case x
  :a "excellent"
  :b "very good"
  :otherwise "failing")

;; another form of the above
(myenum-case x
  (:a "excellent")
  (:b "very good")
  (&  "failing"))