Case macro for the different kinds of type-spec structures.
This is an ACL2::fty sum-type case macro, typically introduced by fty::defflexsum or fty::deftagsum. It allows you to safely check the type of a type-spec structure, or to split into cases based on its type.
In its short form,
(type-spec-case x :void)
is essentially just a safer alternative to writing:
(equal (type-spec-kind x) :void)
Why is using type-spec-case safer? When we directly inspect the
kind with
In its longer form,
(type-spec-case x :void ... :char ... :short ... :int ... :long ... :float ... :double ... :signed ... :unsigned ... :bool ... :complex ... :atomic ... :struct ... :union ... :enum ... :typedef ... :int128 ... :float128 ... :builtin-va-list ... :typeof-expr ... :typeof-type ... :typeof-ambig ...)
It is also possible to consolidate ``uninteresting'' cases using
For convenience, the case macro automatically binds the fields of