Macro verus_exec_expr 

verus_exec_expr!() { /* proc-macro */ }