verus_proof_macro_explicit_exprs!() { /* proc-macro */ }Expand description
verus_proof_macro_explicit_exprs!(f!(tts)) applies verus syntax to transform tts into
tts', then returns f!(tts'), only applying the transform to any of the exprs within it that
are explicitly prefixed with @@, leaving the rest as-is. Contrast this to
[verus_proof_macro_exprs] which is likely what you want to try first to see if it satisfies
your needs.