Rulename
Fixtype of rule names.
This is a product type introduced by fty::defprod.
Fields
- get — common-lisp::stringp
In the abstract syntax,
we use character strings
for the rule names described in [RFC:2.1]
and by the rule rulename in [RFC:4].
We abstract away the restrictions on the characters allowed in rule names,
which [RFC:4] requires to start with a letter
and only use letters, digits, and dashes;
these are ACL2 characters.
These restrictions are captured by the notion of well-formed rule names, which also requires all the letters to be lowercase,
as a normalized representation of rule names,
which are case-insensitive [RFC:2.1].
Subtopics
- Rulenamep
- Recognizer for rulename structures.
- Rulename-fix
- Fixing function for rulename structures.
- Rulename-equiv
- Basic equivalence relation for rulename structures.
- Make-rulename
- Basic constructor macro for rulename structures.
- Rulename->get
- Get the get field from a rulename.
- Change-rulename
- Modifying constructor for rulename structures.
