		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax

Identifier

Fixtype of identifiers.

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

Fields

get — stringp

An identifier is a sequence of characters satisfying certain conditions. For now we use an ACL2 string, wrapped in a one-field product type. ACL2 strings suffice to represent all identifiers, and more. In the future we may add restrictions on the string to be a true identifier as defined in the concrete syntax.

Subtopics

Identifier-fix: Fixing function for identifier structures.
Identifierp: Recognizer for identifier structures.
Identifier-equiv: Basic equivalence relation for identifier structures.
Make-identifier: Basic constructor macro for identifier structures.
Identifier->get: Get the get field from a identifier.
Change-identifier: Modifying constructor for identifier structures.