Macro vstd::prelude::verus_proof_macro_exprs

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

verus_proof_macro_exprs!(f!(exprs)) applies verus syntax to transform exprs into exprs’, then returns f!(exprs’), where exprs is a sequence of expressions separated by “,”, “;”, and/or “=>”.