		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax

Identifier

Fixtype of identifiers.

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

Fields

name — stringp

We use ACL2 strings, which suffice to represent identifiers, and in fact can represent also more than that. This is is not an issue for the abstract syntax (it is only an issue for the concrete syntax), and provides some potential flexibility, e.g. for transforming code.

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->name: Get the name field from a identifier.
Change-identifier: Modifying constructor for identifier structures.