		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax

Hex-string-rest-element

Fixtype of elements of hex strings after the first one.

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

Fields

uscorep — booleanp
pair — hex-pair

The grammar defines the content of a hex string as consisting of zero or more pairs of hex digits, where the pairs may be optionally separated by single underscores. In order to retain that concrete syntax information in the abstract syntax, this fixtype captures the notion of something of the form _hh or hh, where each h is a (potentially different) hex digit. A value of this fixtype represents an element of a hex string, but not the first element, which may not be preceded by underscore.

Subtopics

Hex-string-rest-element-fix: Fixing function for hex-string-rest-element structures.
Hex-string-rest-element-equiv: Basic equivalence relation for hex-string-rest-element structures.
Make-hex-string-rest-element: Basic constructor macro for hex-string-rest-element structures.
Hex-string-rest-element->uscorep: Get the uscorep field from a hex-string-rest-element.
Hex-string-rest-element->pair: Get the pair field from a hex-string-rest-element.
Change-hex-string-rest-element: Modifying constructor for hex-string-rest-element structures.
Hex-string-rest-elementp: Recognizer for hex-string-rest-element structures.