		Search-engine friendly clone of the ACL2 documentation.

Convenience-constructors

Def-rule-const-fn

Signature
(def-rule-const-fn name concatenation-forms) → const-event
Arguments: name — Guard (legal-constantp name).; concatenation-forms — Guard (pseudo-event-form-listp concatenation-forms).
Returns: const-event — Type (pseudo-event-formp const-event).

Definitions and Theorems

Function: def-rule-const-fn

(defun def-rule-const-fn (name concatenation-forms)
 (declare
   (xargs
        :guard (and (legal-constantp name)
                    (pseudo-event-form-listp concatenation-forms))))
 (b*
   ((name-string (symbol-name name))
    (name-chars (explode name-string))
    (name-chars-without-1st-* (cdr name-chars))
    (name-string-without-1st-* (implode name-chars-without-1st-*))
    (const-string (concatenate 'common-lisp::string
                               "*RULE_" name-string-without-1st-*))
    (const-name (intern-in-package-of-symbol const-string name)))
   (cons 'defval
         (cons const-name
               (cons (cons '=_
                           (cons name concatenation-forms))
                     'nil)))))

Theorem: pseudo-event-formp-of-def-rule-const-fn

(defthm pseudo-event-formp-of-def-rule-const-fn
  (b* ((const-event (def-rule-const-fn name concatenation-forms)))
    (pseudo-event-formp const-event))
  :rule-classes :rewrite)