		Search-engine friendly clone of the ACL2 documentation.

Execution

Ensure-boolean

Ensure that an expression value is a boolean.

Signature
(ensure-boolean test env) → bool
Arguments: test — Guard (expr-valuep test).; env — Guard (denvp env).
Returns: bool — Type (boolean-resultp bool).

This is used for tests of conditional expressions and statements, on the expression value resulting from the test expression. We coerce the expression value to a value if needed. We check that the value is a boolean, in which case we return it.

Definitions and Theorems

Function: ensure-boolean

(defun ensure-boolean (test env)
  (declare (xargs :guard (and (expr-valuep test) (denvp env))))
  (let ((__function__ 'ensure-boolean))
    (declare (ignorable __function__))
    (b* (((okf test)
          (expr-value-to-value test env))
         ((unless (value-case test :bool))
          (reserrf (list :non-bool-test (value-fix test)))))
      (value-bool->get test))))

Theorem: boolean-resultp-of-ensure-boolean

(defthm boolean-resultp-of-ensure-boolean
  (b* ((bool (ensure-boolean test env)))
    (boolean-resultp bool))
  :rule-classes :rewrite)

Theorem: ensure-boolean-of-expr-value-fix-test

(defthm ensure-boolean-of-expr-value-fix-test
  (equal (ensure-boolean (expr-value-fix test)
                         env)
         (ensure-boolean test env)))

Theorem: ensure-boolean-expr-value-equiv-congruence-on-test

(defthm ensure-boolean-expr-value-equiv-congruence-on-test
  (implies (expr-value-equiv test test-equiv)
           (equal (ensure-boolean test env)
                  (ensure-boolean test-equiv env)))
  :rule-classes :congruence)

Theorem: ensure-boolean-of-denv-fix-env

(defthm ensure-boolean-of-denv-fix-env
  (equal (ensure-boolean test (denv-fix env))
         (ensure-boolean test env)))

Theorem: ensure-boolean-denv-equiv-congruence-on-env

(defthm ensure-boolean-denv-equiv-congruence-on-env
  (implies (denv-equiv env env-equiv)
           (equal (ensure-boolean test env)
                  (ensure-boolean test env-equiv)))
  :rule-classes :congruence)