Macro vstd::prelude::verus_proof_macro_explicit_exprs

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

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.