		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax

String-element

Fixtype of string elements.

This is a tagged union type, introduced by fty::deftagsum.

Member Tags → Types

:char → string-element-char
:escape → string-element-escape

A string literal consists of a sequence of printable ASCII characters and escapes: these are the string elements we define here. We use ACL2 characters for the former, which can represent all the printable ASCII characters and more; We might restrict the range of characters at some point.

Subtopics

String-element-fix: Fixing function for string-element structures.
String-element-case: Case macro for the different kinds of string-element structures.
String-element-equiv: Basic equivalence relation for string-element structures.
String-elementp: Recognizer for string-element structures.
String-element-escape
String-element-char
String-element-kind: Get the kind (tag) of a string-element structure.