		Search-engine friendly clone of the ACL2 documentation.

Plugging

Rule-prosep

Check if a rule has a single prose value notation as definiens.

Signature
(rule-prosep rule) → yes/no
Arguments: rule — Guard (rulep rule).
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: rule-prosep

(defun rule-prosep (rule)
 (declare (xargs :guard (rulep rule)))
 (b* ((alternation (rule->definiens rule)))
   (and (consp alternation)
        (not (consp (cdr alternation)))
        (b* ((concatenation (car alternation)))
          (and (consp concatenation)
               (not (consp (cdr concatenation)))
               (b* ((repetition (car concatenation))
                    (range (repetition->range repetition))
                    (element (repetition->element repetition)))
                 (and (equal range (repeat-range 1 (nati-finite 1)))
                      (element-case element :prose-val))))))))

Theorem: booleanp-of-rule-prosep

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