Top

Abstract-syntax

Identifier

Fixtype of Syntheto identifiers.

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

Fields

name — stringp

For now we allow any ACL2 string, which is okay for abstract syntax. We will add more restrictions eventually.

Subtopics

Identifierp: Recognizer for identifier structures.
Identifier-fix: Fixing function 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.