		Search-engine friendly clone of the ACL2 documentation.

Convenience-constructors

?_

Construct an option from a variable number of concatenations.

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

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