		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-trees

H-char

Fixtype of characters usable in header names between angle brackets [C17:6.4.7] [C17:A.1.8].

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

Fields

char — natp

This corresponds to h-char in the grammar in [C17].

As explained in abstract-syntax, the natural numbers represent Unicode code points. We wrap the natural number in this fixtype for more abstraction, and to facilitate the addition of restrictions on the number, namely that the character cannot be > or a new-line, but for now we do not capture this restriction.

Subtopics

H-char-fix: Fixing function for h-char structures.
H-char-equiv: Basic equivalence relation for h-char structures.
Make-h-char: Basic constructor macro for h-char structures.
Change-h-char: Modifying constructor for h-char structures.
H-char->char: Get the char field from a h-char.
H-char-p: Recognizer for h-char structures.