		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax

Tag-declon

Fixtype of declarations of structure, union, and enumeration types [C:6.7.2.1] [C:6.7.2.2].

This is a tagged union type, introduced by fty::deftagsum.

Member Tags → Types

:struct → tag-declon-struct
:union → tag-declon-union
:enum → tag-declon-enum

These are declarations that consists of single structure, union, and enumeration specifiers, which introduce structure, union, and enumeration types. These kinds of types are all identified by tags [C:6.2.3], which justifies our choice of name for this fixtype.

These are declarations that include the structure or union members, or the enumerators (which are identifiers). That is, these tag declarations introduce the type with that tag. We only model structure and union members of the form discussed in struct-declon; we only model enumerators that are single identifiers, without bindings to constant expressions.

Subtopics

Tag-declon-fix: Fixing function for tag-declon structures.
Tag-declon-case: Case macro for the different kinds of tag-declon structures.
Tag-declonp: Recognizer for tag-declon structures.
Tag-declon-equiv: Basic equivalence relation for tag-declon structures.
Tag-declon-union
Tag-declon-struct
Tag-declon-enum
Tag-declon-kind: Get the kind (tag) of a tag-declon structure.