		Search-engine friendly clone of the ACL2 documentation.

Convenience-constructors

!_

Construct a group from a variable number of concatenations.

The concatenations are assembled into an alternation, which is the immediate constituent of a group.

Macro: !_

(defmacro !_ (&rest concatenations)
  (cons '!_-fn
        (cons (cons 'list concatenations)
              'nil)))

Definitions and Theorems

Function: !_-fn

(defun !_-fn (alternation)
  (declare (xargs :guard (alternationp alternation)))
  (element-group alternation))

Theorem: elementp-of-!_-fn

(defthm elementp-of-!_-fn
  (b* ((element (!_-fn alternation)))
    (elementp element))
  :rule-classes :rewrite)

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

(defthm !_-fn-of-alternation-fix-alternation
  (equal (!_-fn (alternation-fix alternation))
         (!_-fn alternation)))

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

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