		Search-engine friendly clone of the ACL2 documentation.

Validation-information

Expr-string-info

Fixtype of validation information for string literal expressions.

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

Fields

type — type

This is the type of the annotations that the validator adds to string literal expressions, i.e. the string case of expr. The information for a string literal consists of the type.

Subtopics

Expr-string-info-fix: Fixing function for expr-string-info structures.
Expr-string-info-equiv: Basic equivalence relation for expr-string-info structures.
Make-expr-string-info: Basic constructor macro for expr-string-info structures.
Expr-string-info->type: Get the type field from a expr-string-info.
Change-expr-string-info: Modifying constructor for expr-string-info structures.
Expr-string-infop: Recognizer for expr-string-info structures.