		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-option 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)