		Search-engine friendly clone of the ACL2 documentation.

Files

Structdecl

Fixtype of struct and record declarations.

This is a product type introduced by fty::defprod.

Fields

name — identifier
components — compdecl-list
recordp — booleanp

A struct declaration consists of a name (identifier) and a list of struct component declarations. We do not require the list to be non-empty, at the abstract syntax level.

We also include a boolean flag that says whether the struct type is a record type or not. If the flag is set, we do not require, at the level of abstract syntax, that it has the required components for records; instead, this is enforced in the static semantics.

Subtopics

Structdecl-fix: Fixing function for structdecl structures.
Structdecl-equiv: Basic equivalence relation for structdecl structures.
Make-structdecl: Basic constructor macro for structdecl structures.
Structdeclp: Recognizer for structdecl structures.
Structdecl->components: Get the components field from a structdecl.
Structdecl->recordp: Get the recordp field from a structdecl.
Structdecl->name: Get the name field from a structdecl.
Change-structdecl: Modifying constructor for structdecl structures.