Case macro for the different kinds of tyspec 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 tyspec structure, or to split into cases based on its type.
In its short form,
(tyspec-case x :void)
is essentially just a safer alternative to writing:
(equal (tyspec-kind x) :void)
Why is using tyspec-case safer? When we directly inspect the
kind with
In its longer form,
(tyspec-case x :void ... :char ... :short ... :int ... :long ... :float ... :double ... :signed ... :unsigned ... :bool ... :complex ... :atomic ... :struct ... :union ... :enum ... :tydef ...)
It is also possible to consolidate ``uninteresting'' cases using
For convenience, the case macro automatically binds the fields of