Macro verus_proof_expr

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