		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-multi-expression

Check if a multi-valued expression is statically well-formed.

Signature
(check-multi-expression args args-result) → result
Arguments: args — Guard (expression-listp args).; args-result — Guard (type-resultp args-result).
Returns: result — Type (type-resultp result).

There must be two or more expressions. We return the same type result, unchanged.

Definitions and Theorems

Function: check-multi-expression

(defun check-multi-expression (args args-result)
 (declare (xargs :guard (and (expression-listp args)
                             (type-resultp args-result))))
 (declare
      (xargs :guard (type-result-case args-result
                                      :err t
                                      :ok (= (len args-result.types)
                                             (len args)))))
 (let ((__function__ 'check-multi-expression))
  (declare (ignorable __function__))
  (type-result-case
   args-result
   :err (type-result-err args-result.info)
   :ok
   (if
    (< (len args-result.types) 2)
    (type-result-err
      (list :multi-expression-non-multi (expression-list-fix args)))
    (type-result-fix args-result)))))

Theorem: type-resultp-of-check-multi-expression

(defthm type-resultp-of-check-multi-expression
  (b* ((result (check-multi-expression args args-result)))
    (type-resultp result))
  :rule-classes :rewrite)

Theorem: check-multi-expression-of-expression-list-fix-args

(defthm check-multi-expression-of-expression-list-fix-args
  (equal (check-multi-expression (expression-list-fix args)
                                 args-result)
         (check-multi-expression args args-result)))

Theorem: check-multi-expression-expression-list-equiv-congruence-on-args

(defthm
    check-multi-expression-expression-list-equiv-congruence-on-args
  (implies (expression-list-equiv args args-equiv)
           (equal (check-multi-expression args args-result)
                  (check-multi-expression args-equiv args-result)))
  :rule-classes :congruence)

Theorem: check-multi-expression-of-type-result-fix-args-result

(defthm check-multi-expression-of-type-result-fix-args-result
  (equal (check-multi-expression args (type-result-fix args-result))
         (check-multi-expression args args-result)))

Theorem: check-multi-expression-type-result-equiv-congruence-on-args-result

(defthm
 check-multi-expression-type-result-equiv-congruence-on-args-result
 (implies (type-result-equiv args-result args-result-equiv)
          (equal (check-multi-expression args args-result)
                 (check-multi-expression args args-result-equiv)))
 :rule-classes :congruence)