		Search-engine friendly clone of the ACL2 documentation.

Convenience-constructors

=_-fn

Signature
(=_-fn rulename alternation) → rule
Arguments: rulename — Guard (rulenamep rulename).; alternation — Guard (alternationp alternation).
Returns: rule — Type (rulep rule).

Definitions and Theorems

Function: =_-fn

(defun =_-fn (rulename alternation)
  (declare (xargs :guard (and (rulenamep rulename)
                              (alternationp alternation))))
  (make-rule :name (rulename-fix rulename)
             :incremental nil
             :definiens (alternation-fix alternation)))

Theorem: rulep-of-=_-fn

(defthm rulep-of-=_-fn
  (b* ((rule (=_-fn rulename alternation)))
    (rulep rule))
  :rule-classes :rewrite)

Theorem: =_-fn-of-rulename-fix-rulename

(defthm =_-fn-of-rulename-fix-rulename
  (equal (=_-fn (rulename-fix rulename)
                alternation)
         (=_-fn rulename alternation)))

Theorem: =_-fn-rulename-equiv-congruence-on-rulename

(defthm =_-fn-rulename-equiv-congruence-on-rulename
  (implies (rulename-equiv rulename rulename-equiv)
           (equal (=_-fn rulename alternation)
                  (=_-fn rulename-equiv alternation)))
  :rule-classes :congruence)

Theorem: =_-fn-of-alternation-fix-alternation

(defthm =_-fn-of-alternation-fix-alternation
  (equal (=_-fn rulename (alternation-fix alternation))
         (=_-fn rulename alternation)))

Theorem: =_-fn-alternation-equiv-congruence-on-alternation

(defthm =_-fn-alternation-equiv-congruence-on-alternation
  (implies (alternation-equiv alternation alternation-equiv)
           (equal (=_-fn rulename alternation)
                  (=_-fn rulename alternation-equiv)))
  :rule-classes :congruence)