		Search-engine friendly clone of the ACL2 documentation.

Convenience-constructors

!_-fn

Signature
(!_-fn alternation) → element
Arguments: alternation — Guard (alternationp alternation).
Returns: element — Type (elementp element).

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)