Check if an expression is an expression value.
(expression-valuep expr) → yes/no
This means that the expression is one of the following:
Theorem:
(defthm return-type-of-expression-valuep.yes/no (b* ((?yes/no (expression-valuep expr))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-expression-list-valuep.yes/no (b* ((?yes/no (expression-list-valuep exprs))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-struct-init-valuep.yes/no (b* ((?yes/no (struct-init-valuep cinit))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-struct-init-list-valuep.yes/no (b* ((?yes/no (struct-init-list-valuep cinits))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm expression-valuep-of-expression-fix-expr (equal (expression-valuep (expression-fix expr)) (expression-valuep expr)))
Theorem:
(defthm expression-list-valuep-of-expression-list-fix-exprs (equal (expression-list-valuep (expression-list-fix exprs)) (expression-list-valuep exprs)))
Theorem:
(defthm struct-init-valuep-of-struct-init-fix-cinit (equal (struct-init-valuep (struct-init-fix cinit)) (struct-init-valuep cinit)))
Theorem:
(defthm struct-init-list-valuep-of-struct-init-list-fix-cinits (equal (struct-init-list-valuep (struct-init-list-fix cinits)) (struct-init-list-valuep cinits)))
Theorem:
(defthm expression-valuep-expression-equiv-congruence-on-expr (implies (expression-equiv expr expr-equiv) (equal (expression-valuep expr) (expression-valuep expr-equiv))) :rule-classes :congruence)
Theorem:
(defthm expression-list-valuep-expression-list-equiv-congruence-on-exprs (implies (expression-list-equiv exprs exprs-equiv) (equal (expression-list-valuep exprs) (expression-list-valuep exprs-equiv))) :rule-classes :congruence)
Theorem:
(defthm struct-init-valuep-struct-init-equiv-congruence-on-cinit (implies (struct-init-equiv cinit cinit-equiv) (equal (struct-init-valuep cinit) (struct-init-valuep cinit-equiv))) :rule-classes :congruence)
Theorem:
(defthm struct-init-list-valuep-struct-init-list-equiv-congruence-on-cinits (implies (struct-init-list-equiv cinits cinits-equiv) (equal (struct-init-list-valuep cinits) (struct-init-list-valuep cinits-equiv))) :rule-classes :congruence)