Check if a term may represent a conversion
from an ACL2 boolean to a C
(atc-check-sint-from-boolean term) → (mv erp yes/no arg)
Function:
(defun atc-check-sint-from-boolean (term) (declare (xargs :guard (pseudo-termp term))) (let ((__function__ 'atc-check-sint-from-boolean)) (declare (ignorable __function__)) (b* (((reterr) nil nil) ((acl2::fun (no)) (retok nil nil)) ((mv okp fn args) (fty-check-fn-call term)) ((unless (and okp (eq fn 'sint-from-boolean))) (no)) ((unless (list-lenp 1 args)) (reterr (raise "Internal error: ~x0 not applied to 1 argument." fn)))) (retok t (first args)))))
Theorem:
(defthm booleanp-of-atc-check-sint-from-boolean.yes/no (b* (((mv acl2::?erp ?yes/no ?arg) (atc-check-sint-from-boolean term))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-termp-of-atc-check-sint-from-boolean.arg (b* (((mv acl2::?erp ?yes/no ?arg) (atc-check-sint-from-boolean term))) (pseudo-termp arg)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-term-count-of-atc-check-sint-from-boolean (b* (((mv acl2::?erp ?yes/no ?arg) (atc-check-sint-from-boolean term))) (implies yes/no (< (pseudo-term-count arg) (pseudo-term-count term)))) :rule-classes :linear)