		Search-engine friendly clone of the ACL2 documentation.

Well-formedness

Rulename-wfp

A rule name must start with a lowercase letter (and thus not be empty) and contain only lowercase letters, numbers, and dashes.

Signature
(rulename-wfp rulename) → yes/no
Arguments: rulename — Guard (rulenamep rulename).
Returns: yes/no — Type (booleanp yes/no).

Aside from all letters being lowercase, these constraints are required by the rule rulename in [RFC:4]. The constraint that all letters be lowercase provides a normalized representation of rule names, which are case-insensitive [RFC:2.1].

Definitions and Theorems

Function: rulename-wfp

(defun rulename-wfp (rulename)
  (declare (xargs :guard (rulenamep rulename)))
  (b* ((charstring (rulename->get rulename))
       (chars (explode charstring)))
    (and (consp chars)
         (str::letter-char-p (car chars))
         (str::letter/digit/dash-charlist-p (cdr chars))
         (equal (downcase-charlist chars)
                chars))))

Theorem: booleanp-of-rulename-wfp

(defthm booleanp-of-rulename-wfp
  (b* ((yes/no (rulename-wfp rulename)))
    (booleanp yes/no))
  :rule-classes :rewrite)