Abstract-syntax-irrelevants
Irrelevant values of the abstract syntax fixtypes.
These are nullary operations that return
``irrelevant'' values of the fixtypes that form the abstract syntax,
i.e. values that are never actually used.
For instance, an ACL2 function that returns multiple results,
the first one of which is an error indication,
while the other results include abstract syntax entities,
could return irrelevant values as the latter results
when the first result indicates an error.
The definitions are mostly boilerplate,
except that in some places we put something conveying irrelevance,
e.g. in the definition of irr-ident.
However, this is really unnecessary, and it should be possible to
define all of these according to boilerplate.
This could be an extension of the FTY library;
perhaps every fixtype definition could also generate
some kind of ``default'' value of the fixtype,
which could be used as an irrelevant value in the sense explained above.
For now, we collect these nullary functions in this file and XDOC topic,
to keep the file and XDOC topic of the abstract syntax tidier.
Note that some fixtypes do not have an irrelevant value defined here,
because there are already very short built-in values that can be used,
such as nil for list and option types.
Subtopics
- Irr-amb?-declor/absdeclor
- An irrelevant possibly ambiguous declarators or abstract declarators.
- Irr-typequal/attribspec
- An irrelevant type qualifier or attribute specifier.
- Irr-transunit-ensemble
- An irrelevant ensemble of translation units.
- Irr-declor/absdeclor
- An irrelevant declarator or abstract declarator.
- Irr-asm-stmt
- An irrelevant assembler statement.
- Irr-amb?-expr/tyname
- An irrelevant possibly ambiguous expression or type name.
- Irr-amb?-decl/stmt
- An irrelevant possibly ambiguous declaration or statement.
- Irr-struni-spec
- An irrelevant structure or union specifier.
- Irr-struct-declor
- An irrelevant structure declarator.
- Irr-struct-declon
- An irrelevant structure declaration.
- Irr-stringlit
- An irrelevant string literal.
- Irr-stor-spec
- An irrelevant storage class specifier.
- Irr-statassert
- An irrelevant static assertion declaration.
- Irr-spec/qual
- An irrelevant type specifier or type qualifier.
- Irr-param-declor
- An irrelevant parameter declarator.
- Irr-param-declon
- An irrelevant parameter declaration.
- Irr-member-designor
- An irrelevant member designator.
- Irr-initdeclor
- An irrelevant initializer declarator.
- Irr-ident
- An irrelevant identifier.
- Irr-hex-quad
- An irrelevant quadruple of hexadecimal digits.
- Irr-header-name
- An irrelevant header name.
- Irr-fundef
- An irrelevant function definition.
- Irr-expr/tyname
- An irrelevant expression or type name.
- Irr-enum-spec
- An irrelevant enumeration specifier.
- Irr-dirdeclor
- An irrelevant direct declarator.
- Irr-dirabsdeclor
- An irrelevant direct abstract declarator.
- Irr-desiniter
- An irrelevant initializer with optional designation.
- Irr-decl/stmt
- An irrelevant declaration or statement.
- Irr-decl-spec
- An irrelevant declaration specifier.
- Irr-dec-expo-prefix
- An irrelevant decimal exponent prefix.
- Irr-dec-expo
- An irrelevant decimal exponent.
- Irr-const-expr
- An irrelevant constant expression.
- Irr-comp-stmt
- An irrelevant compound statement.
- Irr-bin-expo-prefix
- An irrelevant binary exponent prefix.
- Irr-bin-expo
- An irrelevant binary exponent.
- Irr-attrib-spec
- An irrelevant attribute specifier.
- Irr-attrib-name
- An irrelevant attribute name.
- Irr-asm-output
- An irrelevant assembler output operand.
- Irr-asm-name-spec
- An irrelevant assembler name specifier.
- Irr-asm-input
- An irrelevant assembler input operand.
- Irr-asm-clobber
- An irrelevant assembler clobber.
- Irr-align-spec
- An irrelevant alignment specifier.
- Irr-absdeclor
- An irrelevant abstract declarator.
- Irr-unop
- An irrelevant unary operator.
- Irr-type-spec
- An irrelevant type specifier.
- Irr-type-qual
- An irrelevant type qualifier.
- Irr-tyname
- An irrelevant type name.
- Irr-transunit
- An irrelevant translation unit.
- Irr-stmt
- An irrelevant statement.
- Irr-label
- An irrelevant label.
- Irr-initer
- An irrelevant initializer.
- Irr-iconst
- An irrelevant integer constant.
- Irr-genassoc
- An irrelevant generic association.
- Irr-fun-spec
- An irrelevant function specifier.
- Irr-extdecl
- An irrelevant external declaration.
- Irr-expr
- An irrelevant expression.
- Irr-escape
- An irrelevant escape.
- Irr-enumer
- An irrelevant enumerator.
- Irr-designor
- An irrelevant designator.
- Irr-declor
- An irrelevant declarator.
- Irr-decl
- An irrelevant declaration.
- Irr-const
- An irrelevant constant.
- Irr-block-item
- An irrelevant block item.
- Irr-binop
- An irrelevant binary operator.
- Irr-attrib
- An irrelevant attribute.
- Irr-asm-qual
- An irrelevant assembler qualifier.
