		Search-engine friendly clone of the ACL2 documentation.

Vl-maybe-scope

Vl-maybe-scope-case

Case macro for the different kinds of vl-maybe-scope structures.

This is an fty sum-type case macro, typically introduced by defflexsum or deftagsum. It allows you to safely check the type of a vl-maybe-scope structure, or to split into cases based on its type.

Short Form

In its short form, vl-maybe-scope-case allows you to safely check the type of a vl-maybe-scope structure. For example:

(vl-maybe-scope-case x :none)

can be used to determine whether x is a none instead of some other kind of vl-maybe-scope structure.

Long Form

In its longer form, vl-maybe-scope-case allows you to split into cases based on the kind of structure you are looking at. A typical example would be:

(vl-maybe-scope-case x
  :none ...
  :some ...)

It is also possible to consolidate ``uninteresting'' cases using :otherwise.

For convenience, the case macro automatically binds the fields of x for you, as appropriate for each case. That is, in the :none case, you can use defprod-style foo.bar style accessors for x without having to explicitly add a none b* binder.