Build a block consisting of a single Java
(jblock-return expr?) → block
Function:
(defun jblock-return (expr?) (declare (xargs :guard (maybe-jexprp expr?))) (let ((__function__ 'jblock-return)) (declare (ignorable __function__)) (list (jstatem-return expr?))))
Theorem:
(defthm jblockp-of-jblock-return (b* ((block (jblock-return expr?))) (jblockp block)) :rule-classes :rewrite)